-- cache.csp
-- Bill Roscoe
-- This is the example from Section 15.2.3, whose main role is to
-- illustrate data-independence arguments involving programs with
-- equality tests.
-- We will find there are two data independent types here: addresses
-- and stored values.
datatype address = A1 | A2 | A3 | A4 | A5 | A6
datatype value = V1 | V2
AA2 = {A1,A2}
AA3 = {A1,A2,A3}
AA4 = {A1,A2,A3,A4}
AA5 = {A1,A2,A3,A4,A5}
AA6 = {A1,A2,A3,A4,A5,A6}
VV2 = {V1,V2}
VV1 = {V1}
channel ra, m_ra:address
channel rv, m_rv:value
channel w, m_w,loc:address.value
-- The parameters of Cache respectively are its state (a list of
-- address/value/bit triples, the types of address and value, and the
-- size of the cache.
-- The cache handles all reads and writes, and where necessary
-- fetches a new value from main memory, or writes back to main
-- memory, to achieve this. For more details see the text:
Cache(ps,A,V,N) = ra?a:A ->
(if elem(a,) then
(rv!val(a,ps) -> Cache(tofront(a,ps),A,V,N))
else if #ps < N then
m_ra!a -> m_rv?v:V -> rv!v ->
Cache(<(a,(v,false))>^ps,A,V,N)
else FlushAndRead(ps,a,A,V,N))
[] w?a:A?v:V ->
if elem(a,) then
Cache(update(a,v,ps),A,V,N)
else if #ps < N then
Cache(<(a,(v,true))>^ps,A,V,N)
else FlushAndWrite(ps,a,v,A,V,N)
-- When a value is removed from the cache, it is written back when
-- it has been written-to since in the cache.
FlushAndRead(ps^<(a',(v',flush))>,a,A,V,N) =
if flush then
m_w!a'!v' -> m_ra!a -> m_rv?v -> rv!v ->
Cache(<(a,(v,false))>^ps,A,V,N)
else
m_ra!a -> m_rv?v -> rv!v ->
Cache(<(a,(v,false))>^ps,A,V,N)
FlushAndWrite(ps^<(a',(v',flush))>,a,v,A,V,N) =
if flush then
m_w!a'!v' -> Cache(<(a,(v,true))>^ps,A,V,N)
else
Cache(<(a,(v,true))>^ps,A,V,N)
-- The functions which manipulate the state:
tofront(a,ps) = <(a',x) | (a',x) <- ps, a'==a>^<(a',x) | (a',x) <- ps, a'!=a>
update(a,v,ps) = <(a,(v,true))>^<(a',x) | (a',x) <- ps, a'!=a>
val(a,ps) = head()
-- The following is the version of the memory that is accurate
-- at only one (settable) address which is described in the text:
OneLoc(A,V) = loc?a:A?v:V -> OneLoc'(a,v,A,V)
OneLoc'(a,v,A,V) = w?a':A?v':V -> (if a==a' then OneLoc'(a,v',A,V)
else OneLoc'(a,v,A,V))
[] ra?a':A -> (if a==a' then rv!v -> OneLoc'(a,v,A,V)
else |~| v':V @ rv!v' -> OneLoc'(a,v,A,V))
-- So the process to test (for refinement of OneLoc) is
Test(A,V,N) = loc?a:A?v:V ->
(Cache(<>,A,V,N)
[m_ra <-> ra, m_rv <-> rv, m_w <-> w] OneLoc'(a,v,A,V))
-- The following is the test which, in the ways explained in the text,
-- establishes the refinement for all larger values of its parameters:
assert OneLoc(AA5,VV2) [FD= Test(AA5,VV2,1)
-- A complete memory, with its state modelled as a set of pairs, is
Memory(f,A,V) = ra?a:A -> rv!apply(f,a) -> Memory(f,A,V)
[] w?a:A?v:V ->
Memory(fnupdate(f,a,v),A,V)
init(v,A) = {(a,v) | a <- A}
apply(f,a) = let pick({x})=x within
pick({v | (a',v) <- f, a'==a})
fnupdate(f,a,v) = union({(a,v)},{(a',v') | (a',v') <- f, a'!=a})
-- Our "real" objective is to show that the following process: the
-- memory enslaved to the cache, refines the memory itself.
Test2(A,V,N) = Cache(<>,A,V,N)
[m_ra <-> ra, m_rv <-> rv, m_w <-> w]
Memory(init(V1,A),A,V)
-- While we can verify examples of this, like
assert Memory(init(V1,AA5),AA5,VV2) [FD= Test2(AA5,VV2,1)
-- this check is not directly amenable to data-independent reasoning in the
-- address datatype and (as discussed in the text) the general case has
-- to be inferred from the OneLoc result above.