Blackbox: Reducing state-space explosion problem

Dealing with model checking is not an easy thing, it can be really greedy in memory and we may encounter state space explosion problem. In order to avoid a such thing, Go2Pins introduces blackbox transitions.

If we take an exemple, with this file:

/* fibonacci.go */
package main

func fibonacci(n int) int {
    n0 := 0
    n1 := 1
    for i := 0; i < n; i++ {
        n2 := n0 + n1
        n0 = n1
        n1 = n2
    }
    return n1
}

func main() {
    fibonacci(5)
}

We can see that we got a program that will produce the 5th term of the Fibonacci’s sequence. If we process fibonacci.go in Go2Pins, we will obtain 34 states and 34 transitions, such as this Kripke Structure:

fibonacci.go Kripke Structure We can easily identify the function call to fibonacci, and it contains 30 states and 30 transitions. Deciding to apply blackbox transformation, will reduce the program’s state space to 4 states and 4 transitions.

If I needed to describre what is a Blackbox brievely, it would be:

  • Packing multiple transitions into a single one.
  • Consider all standard library as Blackboxed.
  • User can specify some functions to be Blackboxed.

Interacting with Global variables in Blackbox transitions

Now that you are more familiar with Go2Pins’ blackbox, we may expose a new problem, our newly blackboxed functions are in the Blackbox library. Accessing a global variables from another library is not common and will generate errors at compile time.

How to interact with global variables inside a Blackboxed functions ?

Starting idea

With this given code:

/* main.go */
package main

var a = 0

func foo() {
    a = 42
}

func main() {
    foo()
}

We want to obtain this:

/* main.go */
package main

import "blackbox"

func G2P_a_set(value int) {
    a = value
}

func main() {
    blackbox.Foo(G2P_a_set)
}

/* blackbox/blackbox.go */
package blackbox

func Foo(G2P_a_set_ptr func(int))  {
    G2P_a_set_ptr(42)
}

In this idea, Global variables are modified via func pointers in order to be accessible from anywhere.

New transformations to treat Global variables

List of transform after global

As you can see, these new transform are applied at the very beginning of Go2Pins’ process, let’s take a look at what it does brievely:

  • PreGlobal transforms will detect all global variables, and in the case no global variables have been detected, the other transforms from the Global’s group are now ignored.
  • Global transform is the main transform from this group. It will make all the changes on the global variables identifier by calling the appropriate accessors functions (getter or setter depending on the context). All functions manipulating global variables will have new arguments, according to these new actions.
  • PostGlobal transform will inherit from the Global transform all new accessors function declarations. It will insert at the beginning of the file these new declarations and will make appropriate changes on the arguments passed as parameters to the functions manipulating global variables.

Recap

Blackbox are great!
But global variables are not handled in it. Thus, the objective is to be able to access global variables from any blackboxed functions.
We found a way to handle it and the first three transforms have been implemented.

Links and more

Lightning talk - February 2021

This work was presented in a Lightning Talk on the 18/02/2021 :

References

  • Kripke, Saul, 1963, “Semantical Considerations on Modal Logic,” Acta Philosophica Fennica, 16: 83-94
  • Alur R., Bouajjani A., Esparza J. (2018) Model Checking Procedural Programs. In: Clarke E., Henzinger T., Veith H., Bloem R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_17
  • Clarke E.M., Klieber W., Nováček M., Zuliani P. (2012) Model Checking and the State Explosion Problem. In: Meyer B., Nordio M. (eds) Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_1