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.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998