clean up of refinement checking

boogie-org · Jan 3, 2020 · 7eddc91 · 7eddc91
1 parent f74c817
commit 7eddc91
Show file tree

Hide file tree

Showing 9 changed files with 284 additions and 346 deletions.
diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs
diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs
diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect
@@ -1,15 +1,11 @@
 bar.bpl(28,3): Error: Non-interference check failed
 Execution trace:
     bar.bpl(7,3): anon0
-    bar.bpl(7,3): anon0_1
     bar.bpl(14,5): inline$AtomicIncr$0$anon0
-    (0,0): YieldChecker
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 bar.bpl(28,3): Error: Non-interference check failed
 Execution trace:
     bar.bpl(38,3): anon0
-    bar.bpl(38,3): anon0_1
-    (0,0): YieldChecker
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
 Boogie program verifier finished with 8 verified, 2 errors
diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect
@@ -1,9 +1,7 @@
 foo.bpl(30,3): Error: Non-interference check failed
 Execution trace:
     foo.bpl(7,3): anon0
-    foo.bpl(7,3): anon0_1
     foo.bpl(14,5): inline$AtomicIncr$0$anon0
-    (0,0): YieldChecker
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
 Boogie program verifier finished with 9 verified, 1 error
diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl
@@ -36,10 +36,10 @@ procedure {:yields} {:layer 1} {:refines "AtomicEnter"} Enter()
     yield;
     while (true) {
         call _old := CAS(0, 1);
-        yield;
         if (_old == 0) {
             break;
         }
+        yield;
         while (true) {
             call curr := Read();
             yield;
@@ -72,4 +72,4 @@ procedure {:atomic} {:layer 1,2} AtomicLeave()
 modifies b;
 { b := 0; }
 
-procedure {:yields} {:layer 0} {:refines "AtomicLeave"} Leave();
+procedure {:yields} {:layer 0} {:refines "AtomicLeave"} Leave();
diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect
@@ -1,9 +1,7 @@
 parallel1.bpl(30,3): Error: Non-interference check failed
 Execution trace:
     parallel1.bpl(7,3): anon0
-    parallel1.bpl(7,3): anon0_1
     parallel1.bpl(14,5): inline$AtomicIncr$0$anon0
-    (0,0): YieldChecker
     (0,0): inline$Impl_YieldChecker_PC_1$0$L0
 
 Boogie program verifier finished with 7 verified, 1 error
diff --git a/Test/civl/refinement.bpl.expect b/Test/civl/refinement.bpl.expect
@@ -2,23 +2,23 @@
 Execution trace:
     refinement.bpl(8,3): anon0
     refinement.bpl(8,3): anon0_2
-    refinement.bpl(43,5): inline$INCR$1$anon0
-    refinement.bpl(8,3): anon0_1
     refinement.bpl(43,5): inline$INCR$0$anon0
-    (0,0): YieldChecker
+    refinement.bpl(8,3): anon0_1
+    refinement.bpl(43,5): inline$INCR$1$anon0
+    (0,0): RefinementChecker
 (0,0): Error: Transition invariant violated in initial state
 Execution trace:
     refinement.bpl(17,3): anon0
     refinement.bpl(17,3): anon0_2
     refinement.bpl(50,5): inline$DECR$0$anon0
-    (0,0): YieldChecker
+    (0,0): RefinementChecker
 (0,0): Error: Transition invariant violated in final state
 Execution trace:
     refinement.bpl(17,3): anon0
     refinement.bpl(17,3): anon0_2
     refinement.bpl(50,5): inline$DECR$0$anon0
     refinement.bpl(17,3): anon0_1
     refinement.bpl(43,5): inline$INCR$0$anon0
-    (0,0): YieldChecker
+    (0,0): RefinementChecker
 
 Boogie program verifier finished with 6 verified, 3 errors
diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect
@@ -3,7 +3,6 @@ Execution trace:
     t1.bpl(99,13): anon0
     t1.bpl(99,13): anon0_1
     t1.bpl(99,13): anon0_1$1
-    (0,0): YieldChecker
     (0,0): inline$Impl_YieldChecker_A_1$0$L1
 
 Boogie program verifier finished with 10 verified, 1 error
diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl
@@ -9,8 +9,6 @@ function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool
  MapConstBool(false)[x := true]
 }
 
-
-
 var {:layer 0,3} H: int;
 var {:layer 0,3} T: int;
 var {:layer 0,3} items: [int]int;
@@ -99,7 +97,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
   var {:layer 3} oldH:int;
   var {:layer 3} oldT:int;
   var {:layer 3} oldStatusT:bool;
-  
+
   yield;
   assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
   assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -114,7 +112,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
   assert {:layer 3} tid == ptTid && t == T;
   assert {:layer 3} oldH <= H && oldT == T;
   assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
-  
+
   call writeItems_put(tid,t, task);
 
   call oldH, oldT := GhostRead();
@@ -126,7 +124,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T);
   assert {:layer 3} oldH <= H && oldT == T;
   assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY);
 
-  
+
   call writeT_put(tid, t+1);
 
   call oldH, oldT := GhostRead();
@@ -162,7 +160,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
   yield;
   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
   assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
-  
+
   while(true)
   invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
   invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -172,7 +170,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs;
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
     assert {:layer 3} oldH <= H && oldT == T;
-    
+
     call t := readT_take_init(tid);
 
     call oldH, oldT := GhostRead();
@@ -182,7 +180,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} t == T;
     assert {:layer 3} items[t-1] == EMPTY ==> H > t-1;
     assert {:layer 3} oldH <= H && oldT == T;
-   
+
     t := t-1;
     call writeT_take(tid, t);
 
@@ -193,7 +191,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} t == T;
     assert {:layer 3} items[t] == EMPTY ==> H > t;
     assert {:layer 3} oldH <= H && oldT == T;
-   
+
     call h := readH_take(tid);
 
     call oldH, oldT := GhostRead();
@@ -208,7 +206,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} h <= H;
     assert {:layer 3} oldH == h;
 
-    if(t<h) {
+    if (t<h) {
       call writeT_take_abort(tid, h);
       task := EMPTY;
 
@@ -233,7 +231,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} T > H ==> items[T] != EMPTY;
     assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs;
 
-    if(t>h) {
+    if (t>h) {
       call takeExitCS(tid);
 
       call oldH, oldT := GhostRead();
@@ -246,7 +244,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     }
     call writeT_take_eq(tid, h+1);
     call oldH, oldT := GhostRead();
-    
+
     yield;
     assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
@@ -255,19 +253,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} oldT == T;
     assert {:layer 3} task == items[t];
     assert {:layer 3} !put_in_cs;
-
-    call chk := CAS_H_take(tid, h,h+1);
 
-    call oldH, oldT := GhostRead();
-    yield;
-    assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY);
-    assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t;
-    assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
-    assert {:layer 3} h+1 == T;
-    assert {:layer 3} task == items[t];
-    assert {:layer 3} !take_in_cs;
-    assert {:layer 3} !put_in_cs;
-    assert {:layer 3} oldH <= H && oldT == T;
+    call chk := CAS_H_take(tid, h,h+1);
 
     if (chk) {
       call oldH, oldT := GhostRead();
@@ -286,7 +273,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs;
     assert {:layer 3} oldH <= H && oldT == T;
   }
-  
+
   call oldH, oldT := GhostRead();
   yield;
   assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs;
@@ -336,7 +323,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
     assert {:layer 3} oldH <= H;
     assert {:layer 3} !steal_in_cs[tid];
-    
+
     call h := readH_steal(tid);
 
     call oldH, oldT := GhostRead();
@@ -350,7 +337,6 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
 
     call t := readT_steal(tid);
 
-
     call oldH, oldT := GhostRead();
     yield;
     assert {:layer 3} steal_in_cs[tid];
@@ -374,9 +360,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
       assert {:layer 3} oldH <= H;
       return;
     }
-
-    call task, taskstatus := readItems(tid, h);
 
+    call task, taskstatus := readItems(tid, h);
 
     call oldH, oldT := GhostRead();
     yield;
@@ -389,6 +374,15 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} h == H ==> status[H] == IN_Q;
 
     call chk := CAS_H_steal(tid, h,h+1);
+    if (chk) {
+      call oldH, oldT := GhostRead();
+      yield;
+      assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
+      assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
+      assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
+      assert {:layer 3} oldH <= H && task != EMPTY;
+      return;
+    }
 
     call oldH, oldT := GhostRead();
     yield;
@@ -399,18 +393,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_
     assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
     assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
     assert {:layer 3} oldH <= H;
-
-    if(chk) {
-      call oldH, oldT := GhostRead();
-      yield;
-      assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid];
-      assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1);
-      assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss);
-      assert {:layer 3} oldH <= H && task != EMPTY;
-      return;
-    }
   }
-   
+
   call oldH, oldT := GhostRead();
   yield;
   assert {:layer 3} chk && task != EMPTY;