Automatic Verification of Software Barriers

Experiments were conducted with Jahob revision 2503 (with backends MONA 1.4-13, Z3 2.19, CVC3 2.2-13), Boogie version 2011-03-17 (with backend Z3 2.15), VCC version 2.3.809.0 (which came with its own versions of Boogie and Z3), and Spin 6.1.0.

Central barrier

• The input to Jahob for the first method.
• The input to Jahob for the second method, namely the free comprehension-cardinality instantiation.
• Commands to start Jahob.
• Most important proof obligations arising from the second input.
• Encountered issues.

Tree-based barriers

Static tree barrier

• The input to Jahob.
• The command to start Jahob.
• Encountered issues.

Combining tree barrier

• The input to Jahob.
• The command to start Jahob.
• Encountered issues.

Array-based barriers

Tournament

• Corrected code.
• The input to Boogie.
• The command to start Boogie.
• Encountered issues.

Dissemination

• The input to Boogie.
• The command to start Boogie.
• Encountered issues.

Real C code

• The input to VCC.
• The command to start VCC.
• Encountered issues.

Barrier on TSO

• Code of the barrier for 1 thread.
• Code of the barrier for 2 threads.
• Code of the barrier for 3 threads.
• Code of the barrier for 4 threads.
• Code of the barrier for 5 threads.
• Code of the barrier for 6 threads.
• Code of the barrier for 7 threads.
• Code of the barrier for 8 threads.
• The command to start verification of all the barriers.
• Encountered issues.

Barrier with its client

• The input to SPIN.
• The commands to start SPIN.
• Encountered issues.