ConcurrentBoogieAndPthreads

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 verificationBoogie @ rise4fun
• A Boogie interpreter Boogaloo
• Some extension of Boogie for concurrency (maybe not what we want)CIVL

Ultimate

• Web interface of Ultimate Automizer
• Installation instructions
• Our workaround for verification of concurrent programs
• Our Boogie extensions

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

First Idea for a Boogie Extension

Add two new statements

Fork Statement

Syntax: fork Expr Id ( Expr* )

Semantics: Call procedure Id as a new thread. First argument: thread identifier, Second argument: name of called procedure, Other arguments: arguments of called procedure

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

Join Statement

Syntax: join Expr

join Id^{,+} := Expr

Semantics: Wait until thread with thread identifier Expr has been finished.

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.