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(m) cache value for location m or bottom.
• Actions:
  • A(a, m, v) assignment a(m) := v.
  • A_pro, A_pro processor read and write request.
  • A_cch, A_cch response to processor requests serviced by the cache.
  • A_get(m), A_fl(m) 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.