Skip to content

ConcurrentBoogieAndPthreads

Jump to bottom
Matthias Heizmann edited this page Sep 27, 2019 · 39 revisions

Concurrent Boogie and Pthreads

Introductory Material

Boogie

  • Boogie specification (noch kein Support für Nebenläufigkeit)This is Boogie 2
  • Microsoft's tool for Boogie verification Boogie@rise4fun
  • A Boogie interpreter Boogaloo
  • Some extension of Boogie for concurrency (maybe not what we want)CIVL

Ultimate

Pthreads

Pthreads in Wikipedia

Example programs that we would like to handle are in the pthreads* subfolders of the SV-COMP C benchmarks

Project Goals

  • 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

Introduction

This page should give you a short overview on the way we handle concurrency. It was our goal to translate a C program, using pthreads, into the Boogie language. To do so we extended the Boogie language by two new statements, the Fork and Join statement. To verify such a program, we also implemented a translation into our CFG.

Terminology

Thread Identifier: We need thread identifiers to differentiate multiple thread instances of the same type. For example if you create two seperate threads that run the same function and you want to join one of them, you must be able to identify which one you want to join. In Boogie a thread identifier can be a single expression or a list of expressions. For pthreads you need to use the pthread_t structure that comes with pthread.

Note that analogously to the Boogie specification we use Id^{,+} to denote a comma-separated list of identifiers.

Fork Statement

Syntax: fork Expr^{,+} Id ( Expr* );

Semantics: Creates a new thread that runs 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.

Join Statement

Syntax: join Expr^{,+} assign Expr^{,+};

We call the first list of expressions the thread identifiers argument and we call the second list of expressions the assigned variables argument.

Semantics: Joins the control-flow of the current thread and another thread. We try to join a thread whose thread identifiers coincide with the values of the thread identifiers argument, and where the number and types of the return values of the thread must fit the given assigned variables argument. The Join statement waits until such a thread has terminated and joins it then. The joining process includes writing the returned values in the assigned variables argument. If a thread has successfully been joined the control-flow of the current thread continues.
If we want to join a thread that has no return values we can omit the assign Expr^{,+} of the statement.
First argument: non-empty list of thread identifiers,
Second argument: non-empty list of expressions.

C-to-Boogie support

pthread_create to fork

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.

pthread_join to join

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;

Boogie-to-CFG support

Fork Statement

Let P be the name of the forked procedure.
For each forked procedure we add two global variables:

  1. thidvar_P - stores the thread identifier or list of thread identifiers for the created thread
  2. th_P_inUse - stores the information if procedure P is currently forked or not

and three edges to the CFG:

  1. One that points to the next location of the current procedure. It is labeled with fork thidvar_P.
  2. 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 variables thidvar_P and th_P_inUse.
  3. and finally the edge pointing to an exception that is raised when the procedure P is already forked.

Example:

Join Statement

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 assigned variables argument in the join statement.

Example:

Tasks

Boogie examples

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.

Clone this wiki locally