Go backward to A Simple Cached Memory
Go up to Top
Go forward to Formal Specification

A Simple Cached Memory (Contd)

A_get( $m$ ) $<=>$ cache( $m$ ) = bottom
and A(cache, $m$ , main( $m$ ))
and Unchanged <op, adr, val, main>
A_cch $<=>$ op = "read" and cache(adr) notequal bottom
and op' = "ready" and val' = cache(adr)
and Unchanged <main, cache>
A_cch $<=>$ op = "write"
and op' = "ready" and A(cache, adr, val)
and Unchanged main
A_fl( $m$ ) $<=>$ cache( $m$ ) notequal bottom
and (op notequal "read" or $m$ notequal adr)
and A(main, $m$ , A( $m$ ))
and A(cache, $m$ , bottom)
and Unchanged <op, adr, val>

Id: tla2.tex,v 1.2 96/05/06 10:48:53 schreine Exp Locker: schreine