@@ -72,19 +72,22 @@ var {:layer 1,3} absMem: [MemAddr]Value;
7272/*
7373The proof is done in two layers.
7474
75- At layer 1, cachePermissions and dirPermissions are introduced allowing dirBusy and cacheBusy
76- to be hidden. At this layer, absMem is also introduced. The main purpose of this layer is to
77- create atomic actions with suitable mover types. Specifically, we want the following:
75+ Layer 1 to layer 2:
76+ absMem is introduced to enable specification of the cache coherence property.
77+ cachePermissions and dirPermissions are introduced allowing dirBusy and cacheBusy to be hidden.
78+ The main purpose of this proof is to create atomic actions with suitable mover types.
79+ Specifically, we want the following:
7880- Memory operations (read and write) to be both movers.
7981- Shared invalidate request at cache to be left mover.
8082- Response to read request at cache to be left mover.
8183- Initiation and conclusion of cache and directory operations to be right and left movers, respectively.
8284
83- At layer 2, we do an invariance proof to hide the directory and all the caches so that the read
84- and write operations at cache are described as atomic operations over absMem. This specfication
85- method naturally captures the cache coherence property. To achieve this specfication, the variables
86- mem, dir, cache, cachePermissions, and dirPermissions are hidden. The yield invariant at this level
87- is a global invariant connecting directory and cache states.
85+ Layer 2 to layer 3:
86+ We do an invariance proof to hide the directory and all the caches so that the read
87+ and write operations at cache are described as atomic operations over absMem.
88+ This specfication method naturally captures the cache coherence property.
89+ To achieve this specfication, the variables mem, dir, cache, cachePermissions, and dirPermissions are hidden.
90+ The yield invariant at this level is a global invariant connecting directory and cache states.
8891*/
8992
9093/// Yield invariants
@@ -116,21 +119,20 @@ invariant (var line := cache[i][Hash(ma)]; (line->state == Invalid() || line->st
116119
117120/// Cache
118121/*
119- There are 5 top-level operations on the cache.
120- cache_read and cache_write read and write a cache entry, respectively;
121- they may nondeterministically choose not to do the operation.
122- cache_evict_req initiates eviction of a cache line.
123- cache_read_shd_req and cache_read_exc_req initiate bringing a memory address into the cache
124- in Shared and Exclusive mode, respectively.
122+ There are 5 top-level operations on the cache:
123+ - cache_read and cache_write read and write a cache entry, respectively.
124+ - cache_evict_req initiates eviction of a cache line.
125+ - cache_read_shd_req and cache_read_exc_req initiate bringing a memory address into the cache
126+ in Shared and Exclusive mode, respectively.
125127The last three operations make asynchronous calls to corresponding operations on the directory
126128to achieve their goals.
127129
128- To specify the protocol, we introduce absMem, a global variable capturing the logical view of
129- memory at layer 1 .
130- The verification demonstrates that cache_read and cache_read do the appropriate operation
131- on absMem.
132- At layer 3, all operations other than cache_read and cache_write disappear by becoming "skip"
133- since all the concrete state is hidden by layer 2 .
130+ We introduce at layer 1 a global variable absMem to capture the logical view of memory.
131+ The presence of absMem allows us to specify the cache coherence property in a natural way .
132+ The verification demonstrates that at layer 3:
133+ - cache_read is abstracted by an atomic action that reads from absMem.
134+ - cache_write is abstracted by an atomic action that writes to absMem.
135+ - all other operations are abstracted by "skip" .
134136*/
135137
136138yield procedure {:layer 2 } cache_read(i: CacheId, ma: MemAddr) returns (result: Option Value)
0 commit comments