source: CIVL/examples/concurrency/locksBad.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: 458 bytes
RevLine 
[9fb69d3]1/* Commandline execution:
2 * civl verify locksBad.cvl
3 * */
[7168bfa]4#include <civlc.cvh>
5
[20d2740]6_Bool lock0 = 0;
7_Bool lock1 = 0;
8
9void proc0() {
10 while (1) {
11 $when (!lock0) lock0=1;
12 $when (!lock1) lock1=1;
13 lock0=0;
14 lock1=0;
15 }
16}
17
18void proc1() {
19 while (1) {
20 $when (!lock1) lock1=1;
21 $when (!lock0) lock0=1;
22 lock0=0;
23 lock1=0;
24 }
25}
26
27void main() {
[48bfab9]28 $proc p0 = $spawn proc0();
29 $proc p1 = $spawn proc1();
30
31 $wait(p0);
32 $wait(p1);
[20d2740]33}
Note: See TracBrowser for help on using the repository browser.