source: CIVL/examples/concurrency/locksGood.cvl

main
Last change on this file was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 513 bytes
Line 
1/* Commandline execution:
2 * civl verify locksGood.cvl
3 * */
4#include<civlc.cvh>
5_Bool lock0 = 0;
6_Bool lock1 = 0;
7
8void proc0() {
9 $atomic {
10 while (1) {
11 $when (!lock0) lock0=1;
12 $when (!lock1) lock1=1;
13 lock0=0;
14 lock1=0;
15 }
16 }
17}
18
19void proc1() {
20 $atomic {
21 while (1) {
22 $when (!lock0) lock0=1;
23 $when (!lock1) lock1=1;
24 lock0=0;
25 lock1=0;
26 }
27 }
28}
29
30void main() {
31 $proc p0 = $spawn proc0();
32 $proc p1 = $spawn proc1();
33
34 $wait(p0);
35 $wait(p1);
36}
Note: See TracBrowser for help on using the repository browser.