[Civl] Cache coherence protocol (#988)

PR contributions:
- Civl construction of a directory-based cache MESI coherence protocol
- Small bug fix in parser

Many important details of the cache coherence protocol are modeled.
- Individual steps taken by the cache and directory controllers are
fine-grained.
- Operations on the cache controller are non-blocking.
- Multiple memory addresses mapping to the same cache address is
modeled.
- Eviction of cache lines is modeled.

Although the overall structure of the code was worked out before
implementation started, several bugs in the implementation were cleaned
up because of the inability to construct a proof.
- Writes must be disallowed if an eviction is in progress.
- The memory address in the cache line must be set by the cache
controller prior to sending the read request to the directory.

The most challenging parts of the proof were the argument that the
shared snoop request and the responses to evict and read requests are
all left movers. Contrary to earlier intuition that the shared snoop is
a right mover, we discovered that instead it is a left mover.

Source/Core/BoogiePL.atg

@@ -1133,15 +1133,19 @@ WhileCmd<out WhileCmd wcmd>
     "invariant"
     { Attribute<ref kv> }
     (
-      Expression<out e> (. if (isFree) {
-                             invariants.Add(new AssumeCmd(z, e, kv));
-                           } else {
-                             invariants.Add(new AssertCmd(z, e, kv));
-                           }
-						   kv = null;
+      Expression<out e> (.
+                          if (isFree) {
+                            invariants.Add(new AssumeCmd(z, e, kv));
+                          } else {
+                            invariants.Add(new AssertCmd(z, e, kv));
+                          }
+						              kv = null;
                         .)
       |
-      CallCmd<out cmd>  (. yields.Add((CallCmd)cmd); .)
+      CallCmd<out cmd>  (.
+                          yields.Add((CallCmd)cmd);
+                          kv = null;
+                        .)
     )
     ";"
   }

Source/Core/Parser.cs

@@ -1667,7 +1667,9 @@ void WhileCmd(out WhileCmd wcmd) {
 
 			} else if (la.kind == 38 || la.kind == 53 || la.kind == 71) {
 				CallCmd(out cmd);
-				yields.Add((CallCmd)cmd); 
+				yields.Add((CallCmd)cmd);
+				kv = null;
+
 			} else SynErr(151);
 			Expect(10);
 		}