Changes between Version 11 and Version 12 of Introduction

Timestamp:

12/29/18 10:02:26 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -157 +157 @@
 }}}
 
-The result of this command is shown in Figure 4.2. The output indicates that a minimal counterexample has length 14, i.e., involves 15 states and 14 transitions (the depth of 19 is five more than 14). It was the 2nd and shortest trace found. It was deemed equivalent to the earlier traces and hence the earlier ones were discarded and only this one saved. We can replay the trace with the command
+which results in the output
+
+{{{
+CIVL v1.18+ of 2018-12-28 -- http://vsl.cis.udel.edu/civl
+
+Violation 0 encountered at depth 21:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:20.32-32
+  $parfor(int i: 0..n-1) dine(i);
+                                ^
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:20.32 ";"
+process 1:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+process 2:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+
+Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
+Restricting search depth to 20
+
+Violation 1 encountered at depth 16:
+CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
+at diningBad.cvl:20.32-32
+  $parfor(int i: 0..n-1) dine(i);
+                                ^
+
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Call stacks:
+process 0:
+  main at diningBad.cvl:20.32 ";"
+process 1:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+process 2:
+  dine at diningBad.cvl:12.4-8 "$when" called from
+  _par_proc0 at diningBad.cvl:20.25-28 "dine"
+
+New log entry is equivalent to previously encountered entry 0
+Length of new trace (16) is less than length of old (21): replacing old with new...
+Restricting search depth to 15
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl verify -inputB=5 -min diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.46
+   memory (bytes)      : 163053568
+   max process count   : 6
+   states              : 96
+   states saved        : 77
+   state matches       : 2
+   transitions         : 91
+   trace steps         : 64
+   valid calls         : 334
+   provers             : cvc4, z3
+   prover calls        : 4
+
+=== Result ===
+The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
+}}}
+
+The output indicates that a minimal counterexample consists of 16 execution steps.   It was the second and shortest trace found. It was deemed equivalent to the earlier traces and hence the earlier ones were discarded and only this one saved. We can replay the trace with the command
 
 {{{
@@ -163 +245 @@
 }}}
 
-The result of this command is shown in Figure 4.3. The output indicates that a deadlock has been found involving 2 philosophers. The trace has 15 transitions; after the initialization sequence, each philosopher picks up her left fork.
+which results in the output
+
+{{{
+CIVL v1.18+ of 2018-12-28 -- http://vsl.cis.udel.edu/civl
+
+Initial state:
+
+State (id=9)
+| Path condition
+| | true
+| Dynamic scopes
+| | dyscope d0 (parent=NULL, static=1)
+| | | variables
+| | | | B = NULL
+| | | | n = NULL
+| | | | forks = NULL
+| Process states
+| | process 0
+| | | call stack
+| | | | Frame[function=main, location=0, diningBad.cvl:1.15 "4", dyscope=d0]
+
+Executed by p0 from State (id=9)
+  0->1: B=5 at diningBad.cvl:1.0-15 "$input int B = 4"
+  1->2: n=InitialValue(n) [n:=X_n] at diningBad.cvl:2.0-11 "$input int n"
+  2->3: $assume((2<=X_n)&&(X_n<=5)) at diningBad.cvl:3.0-20 "$assume(2<=n && n ... )"
+  3->4: forks=InitialValue(forks) [forks:=(boolean[X_n]) ($lambda i: int. false)] at diningBad.cvl:5.0-13 "_Bool forks[n]"
+--> State (id=18)
+
+Step 1: Executed by p0 from State (id=18)
+  4->5: $elaborate_domain(($domain(1))(0..X_n-1#1)) [$assume(0==(X_n - 2))] at diningBad.cvl:19.14-19 "0..n-1"
+--> State (id=22)
+
+Step 2: Executed by p0 from State (id=22)
+  5->6: LOOP_BODY_ENTER (guard: ($domain(1))(0..1#1) has next for (NULL)) at diningBad.cvl:19.14-19 "0..n-1"
+  6->7: NEXT of (NULL) in ($domain(1))(0..1#1) [i:=0] at diningBad.cvl:19.2-5 "$for"
+--> State (id=26)
+
+Step 3: Executed by p0 from State (id=26)
+  7->5: forks[0]=true at diningBad.cvl:19.22-civlc.cvh:10.14 "forks[i] = 1"
+--> State (id=29)
+
+Step 4: Executed by p0 from State (id=29)
+  5->6: LOOP_BODY_ENTER (guard: ($domain(1))(0..1#1) has next for (0)) at diningBad.cvl:19.14-19 "0..n-1"
+  6->7: NEXT of (0) in ($domain(1))(0..1#1) [i:=1] at diningBad.cvl:19.2-5 "$for"
+--> State (id=33)
+
+Step 5: Executed by p0 from State (id=33)
+  7->5: forks[1]=true at diningBad.cvl:19.22-civlc.cvh:10.14 "forks[i] = 1"
+--> State (id=36)
+
+Step 6: Executed by p0 from State (id=36)
+  5->8: LOOP_BODY_EXIT (guard: !($domain(1))(0..1#1) has next for (1)) at diningBad.cvl:19.14-19 "0..n-1"
+--> State (id=38)
+
+Step 7: Executed by p0 from State (id=38)
+  8->9: $elaborate_domain(($domain(1))(0..1#1)) [$assume(true)] at diningBad.cvl:20.17-22 "0..n-1"
+  9->10: $parfor(i0: ($domain(1))(0..1#1)) $spawn _par_proc0(i0) at diningBad.cvl:20.2-8 "$parfor"
+  10->11: _civl_ir1=0 at diningBad.cvl:20.32 ";"
+--> State (id=52)
+
+Step 8: Executed by p0 from State (id=52)
+  11->12: LOOP_BODY_ENTER (guard: 0<2) at diningBad.cvl:20.32 ";"
+--> State (id=54)
+
+Step 9: Executed by p1 from State (id=54)
+  23->15: dine(0) at diningBad.cvl:20.25-31 "dine(i)"
+  15->16: left=0 at diningBad.cvl:8.2-14 "int left = id"
+  16->17: right=(0+1)%2 [right:=1] at diningBad.cvl:9.2-25 "int right = (id  ... n"
+--> State (id=61)
+
+Step 10: Executed by p1 from State (id=61)
+  17->18: LOOP_BODY_ENTER (guard: 1!=0) at diningBad.cvl:10.9 "1"
+--> State (id=63)
+
+Step 11: Executed by p2 from State (id=63)
+  23->15: dine(1) at diningBad.cvl:20.25-31 "dine(i)"
+  15->16: left=1 at diningBad.cvl:8.2-14 "int left = id"
+  16->17: right=(1+1)%2 [right:=0] at diningBad.cvl:9.2-25 "int right = (id  ... n"
+--> State (id=70)
+
+Step 12: Executed by p2 from State (id=70)
+  17->18: LOOP_BODY_ENTER (guard: 1!=0) at diningBad.cvl:10.9 "1"
+--> State (id=72)
+
+Step 13: Executed by p1 from State (id=72)
+  18->19: forks[0]=false at diningBad.cvl:11.24-civlc.cvh:12.15 "forks[left] = 0"
+--> State (id=75)
+
+Step 14: Executed by p2 from State (id=75)
+  18->19: forks[1]=false at diningBad.cvl:11.24-civlc.cvh:12.15 "forks[left] = 0"
+--> State (id=78)
+
+Step 15: 
+State (id=78)
+| Path condition
+| | true
+| Dynamic scopes
+| | dyscope d0 (parent=NULL, static=1)
+| | | variables
+| | | | B = 5
+| | | | n = 2
+| | | | forks = {[0]=false, [1]=false}
+| | dyscope d1 (parent=d0, static=4)
+| | | variables
+| | | | i = 1
+| | | | __LiteralDomain_counter0__ = NULL
+| | dyscope d2 (parent=d0, static=7)
+| | | variables
+| | | | _dom_size0 = 2
+| | | | _par_procs0 = {[0]=p1, [1]=p2}
+| | dyscope d3 (parent=d0, static=8)
+| | | variables
+| | | | i = 0
+| | dyscope d4 (parent=d0, static=8)
+| | | variables
+| | | | i = 1
+| | dyscope d5 (parent=d2, static=9)
+| | | variables
+| | | | _civl_ir1 = 0
+| | dyscope d6 (parent=d5, static=10)
+| | | variables
+| | dyscope d7 (parent=d0, static=3)
+| | | variables
+| | | | id = 0
+| | dyscope d8 (parent=d7, static=12)
+| | | variables
+| | | | left = 0
+| | | | right = 1
+| | dyscope d9 (parent=d0, static=3)
+| | | variables
+| | | | id = 1
+| | dyscope d10 (parent=d9, static=12)
+| | | variables
+| | | | left = 1
+| | | | right = 0
+| Process states
+| | process 0
+| | | call stack
+| | | | Frame[function=main, location=12, diningBad.cvl:20.32 ";", dyscope=d6]
+| | process 1
+| | | call stack
+| | | | Frame[function=dine, location=19, diningBad.cvl:12.4-8 "$when", dyscope=d8]
+| | | | Frame[function=_par_proc0, location=23, diningBad.cvl:20.25-28 "dine", dyscope=d3]
+| | process 2
+| | | call stack
+| | | | Frame[function=dine, location=19, diningBad.cvl:12.4-8 "$when", dyscope=d10]
+| | | | Frame[function=_par_proc0, location=23, diningBad.cvl:20.25-28 "dine", dyscope=d4]
+
+Violation of Deadlock found in (id=78):
+A deadlock is possible:
+  Path condition: true
+  Enabling predicate: false
+process p0 (id=0): false
+process p1 (id=1): false
+process p2 (id=2): false
+
+Trace ends after 15 trace steps.
+Violation(s) found.
+
+=== Source files ===
+diningBad.cvl  (diningBad.cvl)
+
+
+=== Command ===
+civl replay -showTransitions diningBad.cvl 
+
+=== Stats ===
+   time (s)            : 1.44
+   memory (bytes)      : 163053568
+   max process count   : 3
+   states              : 27
+   valid calls         : 100
+   provers             : cvc4, z3
+   prover calls        : 4
+}}}
+
+The output indicates that a deadlock has been found involving 2 philosophers.   After the initialization sequence, each philosopher picks up her left fork.