From dfc417cea131f3e8bb033f3e25b24c94f909c809 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 2 Mar 2018 00:28:56 +0000 Subject: Add address to Write_tag outcome The state monad currently assumes that tags are written to and read from properly aligned addresses (since it does not know the capability size used in the Sail model). This change allows the Sail model to pass in the aligned address(es) even if data is written to an unaligned address. There might be better ways to model tag writing, but this approach seems rather general. --- lib/isabelle/Prompt_monad_lemmas.thy | 6 +++--- lib/isabelle/State_monad_lemmas.thy | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index 2f2d43ef..56aa6e87 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -32,7 +32,7 @@ datatype 'regval event = (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) | e_write_memv "memory_byte list" bool - | e_write_tagv bitU bool + | e_write_tag "bitU list" bitU bool (* Tell the system to dynamically recalculate dependency footprint *) | e_footprint (* Request a memory barrier *) @@ -50,7 +50,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \ 'rv event \ ('rv, 'a, ' | Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \ T" | Excl_res: "((Excl_res k), e_excl_res r, k r) \ T" | Write_memv: "((Write_memv v k), e_write_memv v r, k r) \ T" -| Write_tagv: "((Write_tagv v k), e_write_tagv v r, k r) \ T" +| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \ T" | Footprint: "((Footprint k), e_footprint, k) \ T" | Barrier: "((Barrier bk k), e_barrier bk, k) \ T" | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \ T" @@ -79,7 +79,7 @@ lemma Traces_cases: | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \ Traces" | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \ Traces" | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \ Traces" - | (Write_tagv) val k t' v where "m = Write_tagv val k" and "t = e_write_tagv val v # t'" and "(k v, t', m') \ Traces" + | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \ Traces" | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \ Traces" | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \ Traces" | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \ Traces" diff --git a/lib/isabelle/State_monad_lemmas.thy b/lib/isabelle/State_monad_lemmas.thy index 746fd315..291157f5 100644 --- a/lib/isabelle/State_monad_lemmas.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -274,7 +274,7 @@ lemma no_throw_mem_builtins: "\BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s" "\v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s" "\BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s" - "\t s. ignore_throw (write_tagS t) s = write_tagS t s" + "\BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s" "\s. ignore_throw (excl_resultS ()) s = excl_resultS () s" "\s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s" unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def -- cgit v1.2.3