Merge branch 'master' into irreducible-cfg

Author: shazqadeer

Source/Core/base.bpl

@@ -329,19 +329,19 @@ pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} l: One K, {:li
 pure procedure Map_GetValue<K,V>({:linear} path: Map K V, k: K) returns ({:linear} v: V);
 pure procedure Map_PutValue<K,V>({:linear} path: Map K V, k: K, {:linear_in} v: V);
 
-type Loc;
+type Loc _;
 
-pure procedure {:inline 1} Loc_New() returns ({:linear} {:pool "Loc_New"} l: One Loc)
+pure procedure {:inline 1} Loc_New<V>() returns ({:linear} {:pool "Loc_New"} l: One (Loc V))
 {
   assume {:add_to_pool "Loc_New", l} true;
 }
 
-datatype TaggedLoc<K> { TaggedLoc(loc: Loc, tag: K) }
+datatype TaggedLoc<V,T> { TaggedLoc(loc: Loc V, tag: T) }
 
-pure procedure {:inline 1} TaggedLocSet_New<K>(ks: Set K) returns ({:linear} {:pool "Loc_New"} l: One Loc, {:linear} tagged_locs: Set (TaggedLoc K))
+pure procedure {:inline 1} TaggedLocSet_New<V,T>(tags: Set T) returns ({:linear} {:pool "Loc_New"} l: One (Loc V), {:linear} tagged_locs: Set (TaggedLoc V T))
 {
   assume {:add_to_pool "Loc_New", l} true;
-  tagged_locs := Set((lambda x: TaggedLoc K :: x->loc == l->val && Set_Contains(ks, x->tag)));
+  tagged_locs := Set((lambda x: TaggedLoc V T :: x->loc == l->val && Set_Contains(tags, x->tag)));
 }
 
 procedure create_async<T>(PA: T);

Source/Core/node.bpl

@@ -1,76 +1,77 @@
-datatype Node<K,T> { Node(next: Option K, val: T) }
+datatype Node<T> { Node(next: Option (Loc (Node T)), val: T) }
+type LocNode T = Loc (Node T);
 
-function Between<K,T>(f: [K]Node K T, x: Option K, y: Option K, z: Option K): bool;
-function Avoiding<K,T>(f: [K]Node K T, x: Option K, y: Option K, z: Option K): bool;
-function {:inline} BetweenSet<K,T>(f:[K]Node K T, x: Option K, z: Option K): [K]bool
+function Between<T>(f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T))): bool;
+function Avoiding<T>(f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T))): bool;
+function {:inline} BetweenSet<T>(f:[Loc (Node T)]Node T, x: Option (Loc (Node T)), z: Option (Loc (Node T))): [Loc (Node T)]bool
 {
-  (lambda y: K :: Between(f, x, Some(y), z))
+  (lambda y: Loc (Node T) :: Between(f, x, Some(y), z))
 }
 
 // reflexive
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K :: Between(f, x, x, x));
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)) :: Between(f, x, x, x));
 
 // step
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T) ::
   {f[x]} 
   Between(f, Some(x), f[x]->next, f[x]->next));
 
 // reach
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T), y: Option (Loc (Node T)) ::
   {f[x], Between(f, Some(x), y, y)} 
   Between(f, Some(x), y, y) ==> Some(x) == y || Between(f, Some(x), f[x]->next, y));
 
 // cycle
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Loc (Node T), y: Option (Loc (Node T)) ::
   {f[x], Between(f, Some(x), y, y)} 
   f[x]->next == Some(x) && Between(f, Some(x), y, y) ==> Some(x) == y);
 
 // sandwich
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)) ::
   {Between(f, x, y, x)} 
   Between(f, x, y, x) ==> x == y);
 
 // order1
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, y), Between(f, x, z, z)} 
   Between(f, x, y, y) && Between(f, x, z, z) ==> Between(f, x, y, z) || Between(f, x, z, y));
 
 // order2
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, z)} 
   Between(f, x, y, z) ==> Between(f, x, y, y) && Between(f, y, z, z));
 
 // transitive1
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, y), Between(f, y, z, z)} 
   Between(f, x, y, y) && Between(f, y, z, z) ==> Between(f, x, z, z));
 
 // transitive2
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K, w: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)), w: Option (Loc (Node T)) ::
   {Between(f, x, y, z), Between(f, y, w, z)} 
   Between(f, x, y, z) && Between(f, y, w, z) ==> Between(f, x, y, w) && Between(f, x, w, z));
 
 // transitive3
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K, w: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)), w: Option (Loc (Node T)) ::
   {Between(f, x, y, z), Between(f, x, w, y)} 
   Between(f, x, y, z) && Between(f, x, w, y) ==> Between(f, x, w, z) && Between(f, w, y, z));
 
 // This axiom is required to deal with the incompleteness of the trigger for the reflexive axiom.
 // It cannot be proved using the rest of the axioms.
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, u: Option K, x: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, u: Option (Loc (Node T)), x: Option (Loc (Node T)) ::
   {Between(f, u, x, x)} 
   Between(f, u, x, x) ==> Between(f, u, u, x));
 
 // relation between Avoiding and Between
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Avoiding(f, x, y, z)} 
   Avoiding(f, x, y, z) <==> Between(f, x, y, z) || (Between(f, x, y, y) && !Between(f, x, z, z)));
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, x: Option K, y: Option K, z: Option K :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, x: Option (Loc (Node T)), y: Option (Loc (Node T)), z: Option (Loc (Node T)) ::
   {Between(f, x, y, z)} 
   Between(f, x, y, z) <==> Avoiding(f, x, y, z) && Avoiding(f, x, z, z));
 
 // update
-axiom {:ctor "Node"} (forall<K,T> f: [K]Node K T, u: Option K, v: Option K, x: Option K, p: K, q: Node K T :: 
+axiom {:ctor "Node"} (forall<T> f: [Loc (Node T)]Node T, u: Option (Loc (Node T)), v: Option (Loc (Node T)), x: Option (Loc (Node T)), p: Loc (Node T), q: Node T ::
   {Avoiding(f[p := q], u, v, x)} 
   Avoiding(f[p := q], u, v, x) <==>
     (Avoiding(f, u, v, Some(p)) && Avoiding(f, u, v, x)) || 

Test/civl/large-samples/GC.bpl

@@ -2,7 +2,7 @@
 // Copyright (c) Microsoft Corporation.  All rights reserved.
 //
 
-// RUN: %parallel-boogie -lib:set_size "%s" > "%t"
+// RUN: %parallel-boogie -lib:set_size -timeLimit:0 -vcsSplitOnEveryAssert "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Tid(i, ps) represents a linear thread id for thread number i, where i > 0 and ps = {Left(i), Right(i)}.

Test/civl/large-samples/cache-coherence.bpl

@@ -623,43 +623,50 @@ preserves call YieldInv#2();
 requires call YieldRead(i, ma, drp);
 {
   var dirState: DirState;
-  var value: Value;
   var {:linear} {:layer 1,2} dp: Set DirPermission;
-  var {:linear} {:layer 1,2} dpOne: Set DirPermission;
-  var victims: Set CacheId;
-  var victim: CacheId;
-  var {:layer 2} cache_s: [CacheId][CacheAddr]CacheLine;
+  var value: Value;
 
   par dirState, dp := dir_req_begin(ma) | YieldInv#1();
   if (dirState is Owner) {
     par value := cache_invalidate_exc#1(dirState->i, ma, Invalid(), dp) | YieldInv#1();
     par write_mem(ma, value, dp) | YieldInv#1();
   } else {
-    call {:layer 2} cache_s := Copy(cache);
-    victims := dirState->iset;
-    while (victims != Set_Empty())
-    invariant {:yields} {:layer 1} true;
-    invariant {:layer 1} call YieldInv#1();
-    invariant {:layer 2} dp == WholeDirPermission(ma);
-    invariant {:layer 2} Set_IsSubset(victims, dirState->iset);
-    invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) || cache[i] == cache_s[i]);
-    invariant {:layer 2} (forall i: CacheId:: Set_Contains(dirState->iset, i) ==> 
-                            if Set_Contains(victims, i)
-                            then cache[i] == cache_s[i]
-                            else cache[i] == cache_s[i][Hash(ma) := CacheLine(ma, cache_s[i][Hash(ma)]->value, Invalid())]);
-    {
-      victim := Choice(victims->val);
-      victims := Set_Remove(victims, victim);
-      par dpOne, dp := get_victim(victim, ma, dp) | YieldInv#1();
-      par cache_invalidate_shd#1(victim, ma, Invalid(), dpOne) | YieldInv#1();
-      par dp := put_victim(dpOne, dp) | YieldInv#1();
-    }
+    par dp := invalidate_sharers(ma, dirState->iset, dp) | YieldInv#1();
     par value := read_mem(ma, dp) | YieldInv#1();
   }
   call cache_read_resp#1(i, ma, value, Exclusive(), drp, dp);
   par dir_req_end(ma, Owner(i), dp) | YieldInv#1();
 }
 
+yield left procedure {:layer 2} invalidate_sharers(ma: MemAddr, victims: Set CacheId, {:linear_in} {:layer 1,2} dp: Set DirPermission)
+  returns ({:linear} {:layer 1,2} dp': Set DirPermission)
+modifies cache;
+requires {:layer 2} Set_IsSubset(Set((lambda x: DirPermission :: Set_Contains(victims, x->i) && x->ma == ma)), dp);
+requires {:layer 2} (forall i: CacheId, ca: CacheAddr:: (var line := cache[i][ca];
+                      line->state == Invalid() ||
+                      (line->value == absMem[line->ma] && if line->state == Shared() then dir[line->ma] is Sharers else dir[line->ma] is Owner)));
+requires {:layer 2} (forall i: CacheId:: Set_Contains(victims, i) ==> cache[i][Hash(ma)]->state == Shared() && cache[i][Hash(ma)]->ma == ma);
+ensures {:layer 2} (forall i: CacheId:: Set_Contains(victims, i) ==> 
+                        cache[i] == old(cache)[i][Hash(ma) := CacheLine(ma, old(cache)[i][Hash(ma)]->value, Invalid())]);
+ensures {:layer 2} (forall i: CacheId:: Set_Contains(victims, i) || cache[i] == old(cache)[i]);
+ensures {:layer 2} dp == dp';
+{
+  var victim: CacheId;
+  var victims': Set CacheId;
+  var {:linear} {:layer 1,2} dpOne: Set DirPermission;
+
+  dp' := dp;
+  if (victims == Set_Empty())
+  {
+    return;
+  }
+  victim := Choice(victims->val);
+  victims' := Set_Remove(victims, victim);
+  par dpOne, dp' := get_victim(victim, ma, dp');
+  par cache_invalidate_shd#1(victim, ma, Invalid(), dpOne) | dp' := invalidate_sharers(ma, victims', dp');
+  par dp' := put_victim(dpOne, dp');
+}
+
 yield procedure {:layer 1} get_victim(victim: CacheId, ma: MemAddr, {:layer 1} {:linear_in} dp: Set DirPermission)
 returns ({:linear} {:layer 1} dpOne: Set DirPermission, {:linear} {:layer 1} dp': Set DirPermission)
 refines both action {:layer 2} _ {

Test/civl/large-samples/cache-coherence.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 91 verified, 0 errors
+Boogie program verifier finished with 93 verified, 0 errors