[Civl] Cache coherence protocol

[shazqadeer]

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.