Go backward to Quantification in TLA
Go up to Top
Go forward to A Simple Cached Memory
Refinement Mappings
- Implementation of memory interface.
- exists memory: Phi.
- Main memory main and cache memory cache.
- cache() cache value for location or bottom.
- Actions:
- A(, , ) assignment := .
- A, A processor read and
write request.
- A, A response to processor requests
serviced by the cache.
- A(), A() moving value from
memory to cache and flushing value from cache to memory.
- A next-state relation (disjunctions of all actions).
- A disjunction of memory actions.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine