vmurali / seqconsistency Goto Github PK

This repository contains the proof of a full system implementing sequential
consistency. The proof is modular in the sense that we prove that an arbitrary
tree hierarchy of caches implements an instantaneous atomic memory, and a
speculative out-of-order processor implements an instantaneous atomic
processor. The final theorem states that when multiple such speculative
processors are connected to the hierarchy of caches, then it implements several
atomic processors connected to memory.

The cache proof is present in the cache folder. BaseTree.v and Tree.v files
contains the inductive definition for trees and the cache hierarchies are
instances of trees. Tree.v is a named version of BaseTree with each node having
a name computed based on the position of the node w.r.t. root of the tree.
Hier.v and HierProperties.v contains a list of properties about tree
hierarchies.  Caches/DataTypes.v and MsiState.v contains the definition of some
of the datatypes used in the caches. Cache.v contains the invariants related to
internal caches and the root while L1.v and LatestValue.v contains the
invariants related to the leaf caches. CommonBeh record inside Cache.v captures
the trivial invariants that can be obtained by simply examining the state
transitions of the caches (given in Rules.v), and the proofs of these trivial
invariants are in BehaviorAxioms.v. LatestValue.v contains theorems which
pertain to establishing that any non-I address in a cache contains the latest
value (given by the last store from any processor to that address).
LatestValueAxiom.v proves some helper theorems in LatestValue.v file.
Channel.v defines the communication channel between the caches, represented
using unbounded lists. ChannelAxiom.v and ChannelAxiomHelp.v contains
invariants regarding the channels. Top.v assembles the whole system by
combining the internal caches with the L1 caches and the channels and proves
the store-atomicity theorem (which states that any load reads the latest store
from any processor).

TransitionsNew.v in the top-level directory defines the semantics of the
transition system and the speculative processor is implemented in FreshNew.v.
The speculative processor's implementation is not concrete -- it abstracts
over the ISA and does not have a concrete implementation of a reorder buffer
or branch predictors (instead their behaviors are encapsulated directly in the
preconditions in the state transitions). StoreAtomicity.v shows that any
system that obeys the store-atomicity theorem implements instantaneous memory,
where loads read values from the memory instantaneously and stores update the
corresponding location instantaneously.

Useful.v and Caches.Useful.v contain useful generic lemmas which are used at
various places in this project (e.g. facts about lists that are not present in
the standard library).

Two things to note:
a) When this framework was being developed, I did not know much about proof
automation, so most of the proofs contain a lot of tedious details spelt out.
Moreover, I was also learning Coq at that point, so things could have been
designed differently if I were to start it again (which is what I am doing with
Kami).
b) The Processor part and the Cache part were developed completely
orthogonally, with no foreseen plan to integrate them. So a lot of code has
been copied and pasted between these two parts.