ConcurrentBoogieAndPthreads
- Boogie specification (noch kein Support für Nebenläufigkeit)This is Boogie 2
- Microsoft's tool for Boogie verificationBoogie @ rise4fun
- A Boogie interpreter Boogaloo
- Some extension of Boogie for concurrency (maybe not what we want)CIVL
- Web interface of Ultimate Automizer
- Installation instructions
- Our workaround for verification of concurrent programs
- Our Boogie extensions
Example programs that we would like to handle are in the pthreads* subfolders of the SV-COMP C benchmarks
- Erweitere Boogie in Ultimate um Support für Nebenläufigkeit.
- Erweitere unseren Boogie AST um neue Sprachkonstrukte.
- Erweitere unseren Boogie Parser.
- Erweitere unsere Boogie-zu-Boogie Transformationen um Support für neue Sprachkonstrukte.
- Erweitere unsere Boogie-zu-Kontrollflußgraph um Support für neue Sprachkonstrukte.
- Erweitere unsere C-zu-Boogie Übersetzung um Support für pthread.
- Create a document or wikipage that documents our extension
Add two new statements
Note that analogously to the Boogie specification we use Id^{,+} to denote a comma-separated list of identifiers.
Syntax: fork Expr^{,+} Id ( Expr* );
Semantics: Creates a new thread that invokes the Id procedure.
First argument: non-empty list of thread identifier,
Second argument: name of the called procedure,
Other arguments: arguments of the called procedure.
Syntax: join Expr^{,+} assign Expr^{,+};
Semantics: Waits for the thread with the identifier Expr^{,+} to terminate. If the thread has already terminated, then it returns immediately.
If the thread returns no value, the assign Expr^{,+} part can be omitted. Otherwise the return value will be written to the Expr^{,+}. Note that the number of return values must fit the numbers of expression given.
First argument: non-empty list of thread identifier,
Second argument: non-empty list of expressions.
C-Syntax: pthread_create(pthread_t *tid, const pthread_attr_t *attr, void *(*foo) (void *), void *x);
We translate the given pthread_create statement from C into the following boogie statement:
fork tid foo(x);
Semantics: Here, tid becomes an integer variable to identify the created thread and x points to a location in the memory. Currently we ignore the second argument *attr of pthread_create.
C-Syntax: pthread_join(pthread_t tid, void **retval);
We translate the given pthread_join statement from C into the following boogie statement:
join tid assign retval;
Semantics: Here, tid becomes an integer variable and retval is a pointer. If the second argument of pthread_join is NULL or 0, we translate the statement just into join tid;
Let P be the name of the forked procedure.
For each forked procedure we add two global variables:
-
thidvar_P- stores the identifier or list of identifiers for the created thread -
th_P_inUse- stores the information if procedure P is currently forked or not
and three edges to the CFG:
- One that points to the next location of the current procedure. It is labeled with
fork thidvar_P. - Another that points to the entry location of the forked procedure. This edge is labeled with the actual fork statement (here
fork x foo(y, z)). It also assigns the global variablesthidvar_Pandth_P_inUse. - and finally the edge pointing to an exception that is raised when the procedure P is already forked.
Let P be the name of the forked procedure.
For each join statement we add one edge from each exit location of a potential forked procedure.
A potential procedure has the same number and types of expressions in the thidvar_P variable as the given arguments in the join statement.
Implement algorithms that solve the mutual exclusion problem and implement them in our (extended) Boogie language. Take e.g., the algorithms that have already been implemented in our webinterface. We will use these examples as regression tests.