header {*
\chapter{The generic multithreaded semantics}
\isaheader{State of the multithreaded semantics} *}
theory FWState imports
"../Common/Aux"
begin
datatype lock_action =
Lock
| Unlock
| UnlockFail
| ReleaseAcquire
datatype ('t,'x,'m) new_thread_action =
NewThread 't 'x 'm
| NewThreadFail
| ThreadExists 't
datatype 't conditional_action = Join 't
datatype 'w wait_set_action =
Suspend 'w
| Notify 'w
| NotifyAll 'w
types 'l lock_actions = "'l =>f lock_action list"
translations
"lock_actions l" <= (type) "l =>f lock_action list"
types ('l,'t,'x,'m,'w,'o) thread_action =
"'l lock_actions × ('t,'x,'m) new_thread_action list ×
't conditional_action list × 'w wait_set_action list × 'o"
print_translation {*
let
fun tr' [Const ("finfun", _) $ l $ (Const ("list", _) $ Const ("lock_action", _)),
Const ("*",_) $ (Const ("list", _) $ (Const ("new_thread_action", _) $ t1 $ x $ m)) $
(Const ("*", _) $ (Const ("list", _) $ (Const ("conditional_action", _) $ t2)) $
(Const ("*", _) $ (Const ("list", _) $ (Const ("wait_set_action", _) $ w)) $ o1))] =
if t1 = t2 then Syntax.const "thread_action" $ l $ t1 $ x $ m $ w $ o1
else raise Match;
in [("*",tr')]
end
*}
definition locks_a :: "('l,'t,'x,'m,'w,'o) thread_action => 'l lock_actions" ("\<lbrace>_\<rbrace>l" [0] 1000) where
"locks_a ≡ fst"
definition thr_a :: "('l,'t,'x,'m,'w,'o) thread_action => ('t,'x,'m) new_thread_action list" ("\<lbrace>_\<rbrace>t" [0] 1000) where
"thr_a ≡ fst o snd"
definition cond_a :: "('l,'t,'x,'m,'w,'o) thread_action => 't conditional_action list" ("\<lbrace>_\<rbrace>c" [0] 1000) where
"cond_a = fst o snd o snd"
definition wset_a :: "('l,'t,'x,'m,'w,'o) thread_action => 'w wait_set_action list" ("\<lbrace>_\<rbrace>w" [0] 1000)where
"wset_a ≡ fst o snd o snd o snd"
definition obs_a :: "('l,'t,'x,'m,'w,'o) thread_action => 'o" ("\<lbrace>_\<rbrace>o" [0] 1000) where
"obs_a ≡ snd o snd o snd o snd"
lemma locks_a_conv [simp]: "locks_a (ls, ntsjswss) = ls"
by(simp add:locks_a_def)
lemma thr_a_conv [simp]: "thr_a (ls, nts, jswss) = nts"
by(simp add: thr_a_def)
lemma cond_a_conv [simp]: "cond_a (ls, nts, js, wws) = js"
by(simp add: cond_a_def)
lemma wset_a_conv [simp]: "wset_a (ls, nts, js, wss, obs) = wss"
by(simp add: wset_a_def)
lemma obs_a_conv [simp]: "obs_a (ls, nts, js, wss, obs) = obs"
by(simp add: obs_a_def)
fun ta_update_locks :: "('l,'t,'x,'m,'w,'o) thread_action => lock_action => 'l => ('l,'t,'x,'m,'w,'o) thread_action" where
"ta_update_locks (ls, nts, js, wss, obs) lta l = (ls(f l := lsf l @ [lta]), nts, js, wss, obs)"
fun ta_update_NewThread :: "('l,'t,'x,'m,'w,'o) thread_action => ('t,'x,'m) new_thread_action => ('l,'t,'x,'m,'w,'o) thread_action" where
"ta_update_NewThread (ls, nts, js, wss, obs) nt = (ls, nts @ [nt], js, wss, obs)"
fun ta_update_Conditional :: "('l,'t,'x,'m,'w,'o) thread_action => 't conditional_action => ('l,'t,'x,'m,'w,'o) thread_action"
where
"ta_update_Conditional (ls, nts, js, wss, obs) j = (ls, nts, js @ [j], wss, obs)"
fun ta_update_wait_set :: "('l,'t,'x,'m,'w,'o) thread_action => 'w wait_set_action => ('l,'t,'x,'m,'w,'o) thread_action" where
"ta_update_wait_set (ls, nts, js, wss, obs) ws = (ls, nts, js, wss @ [ws], obs)"
fun ta_update_obs :: "('l,'t,'x,'m,'w,'o option) thread_action => 'o => ('l,'t,'x,'m,'w,'o option) thread_action" ("_\<lbrace>o_\<rbrace>" [1000,0] 1000)
where
"ta_update_obs (ls, nts, js, wss, obs) ob = (ls, nts, js, wss, Some ob)"
abbreviation empty_ta :: "('l,'t,'x,'m,'w,'o option) thread_action" ("ε") where
"empty_ta ≡ (λf [], [], [], [], None)"
nonterminals
locklets locklet
syntax
"_locklet" :: "lock_action => 'l => locklet" ("(2_/->_)")
"" :: "locklet => locklets" ("_")
"_locklets" :: "locklet => locklets => locklets" ("_,/ _")
"_lockUpdate" :: "'a => locklets => 'a" ("_\<lbrace>l/(_)\<rbrace>" [1000,0] 1000)
translations
"_lockUpdate ta (_locklets b bs)" == "_lockUpdate (_lockUpdate ta b) bs"
"ta\<lbrace>lx->y\<rbrace>" == "(CONST ta_update_locks) ta x y"
nonterminals
ntlets ntlet
syntax
"_ntlet" :: "('t,'m,'x) new_thread_action => ntlet" ("(_)")
"" :: "ntlet => ntlets" ("_")
"_ntlets" :: "ntlet => ntlets => ntlets" ("_,/ _")
"_ntUpdate" :: "'a => ntlets => 'a" ("_\<lbrace>t/(_)\<rbrace>" [1000,0] 1000)
translations
"_ntUpdate ta (_ntlets b bs)" == "_ntUpdate (_ntUpdate ta b) bs"
"ta\<lbrace>tnt\<rbrace>" == "(CONST ta_update_NewThread) ta nt"
nonterminals
jlets jlet
syntax
"_jlet" :: "'t conditional_action => jlet" ("(_)")
"" :: "jlet => jlets" ("_")
"_jlets" :: "jlet => jlets => jlets" ("_,/ _")
"_jUpdate" :: "'a => jlets => 'a" ("_\<lbrace>c/(_)\<rbrace>" [1000,0] 1000)
translations
"_jUpdate ta (_jlets b bs)" == "_jUpdate (_jUpdate ta b) bs"
"ta\<lbrace>cnt\<rbrace>" == "(CONST ta_update_Conditional) ta nt"
nonterminals
wslets wslet
syntax
"_wslet" :: "'w wait_set_action => wslet" ("(_)")
"" :: "wslet => wslets" ("_")
"_wslets" :: "wslet => wslets => wslets" ("_,/ _")
"_wsUpdate" :: "'a => wslets => 'a" ("_\<lbrace>w/(_)\<rbrace>" [1000,0] 1000)
translations
"_wsUpdate ta (_wslets b bs)" == "_wsUpdate (_wsUpdate ta b) bs"
"ta\<lbrace>wws\<rbrace>" == "(CONST ta_update_wait_set) ta ws"
types
't lock = "('t × nat) option"
('l,'t) locks = "'l =>f 't lock"
'l released_locks = "'l =>f nat"
('l,'t,'x) thread_info = "'t \<rightharpoonup> ('x × 'l released_locks)"
('w,'t) wait_sets = "'t \<rightharpoonup> 'w"
('l,'t,'x,'m,'w) state = "('l,'t) locks × (('l,'t,'x) thread_info × 'm) × ('w,'t) wait_sets"
translations
"locks l t" <= (type) "l =>f (t × nat) option"
"thread_info l t x" <= (type) "t \<rightharpoonup> (x × (l =>f nat))"
print_translation {*
let
fun tr' [Const ("finfun", _) $ l1 $ (Const ("option", _) $ (Const ("*", _) $ t1 $ Const ("nat", _))),
Const ("*", _) $
(Const ("*", _) $ (Const ("fun", _) $ t2 $
(Const ("option", _) $ (Const ("*", _) $ x $
(Const ("finfun", _) $ l2 $ Const ("nat", _))))) $ m) $
(Const ("fun", _) $ t3 $ (Const ("option", _) $ w))] =
if t1 = t2 andalso t1 = t3 andalso l1 = l2
then Syntax.const "state" $ l1 $ t1 $ x $ m $ w
else raise Match;
in [("*",tr')]
end
*}
abbreviation no_wait_locks :: "'l =>f nat"
where "no_wait_locks ≡ (λf 0)"
lemma neq_no_wait_locks_conv:
"ln ≠ no_wait_locks <-> (∃l. lnf l > 0)"
by(auto simp add: expand_finfun_eq expand_fun_eq)
lemma neq_no_wait_locksE:
assumes "ln ≠ no_wait_locks" obtains l where "lnf l > 0"
using assms
by(auto simp add: neq_no_wait_locks_conv)
definition locks :: "('l,'t,'x,'m,'w) state => ('l,'t) locks" where
"locks lstsmws ≡ fst lstsmws"
definition thr :: "('l,'t,'x,'m,'w) state => ('l,'t,'x) thread_info" where
"thr lstsmws ≡ fst (fst (snd lstsmws))"
definition shr :: "('l,'t,'x,'m,'w) state => 'm" where
"shr lstsmws ≡ snd (fst (snd lstsmws))"
definition wset :: "('l,'t,'x,'m,'w) state => ('w,'t) wait_sets" where
"wset lstsmws ≡ snd (snd lstsmws)"
lemma locks_conv [simp]: "locks (ls, tsmws) = ls"
by(simp add: locks_def)
lemma thr_conv [simp]: "thr (ls, (ts, m), ws) = ts"
by(simp add: thr_def)
lemma shr_conv [simp]: "shr (ls, (ts, m), ws) = m"
by(simp add: shr_def)
lemma wset_conv [simp]: "wset (ls, (ts, m), ws) = ws"
by(simp add: wset_def)
primrec convert_new_thread_action :: "('x => 'x') => ('t,'x,'m) new_thread_action => ('t,'x','m) new_thread_action"
where
"convert_new_thread_action f (NewThread t x m) = NewThread t (f x) m"
| "convert_new_thread_action f (ThreadExists t) = ThreadExists t"
| "convert_new_thread_action f NewThreadFail = NewThreadFail"
lemma convert_new_thread_action_inv [simp]:
"NewThread t x h = convert_new_thread_action f nta <-> (∃x'. nta = NewThread t x' h ∧ x = f x')"
"ThreadExists t = convert_new_thread_action f nta <-> nta = ThreadExists t"
"NewThreadFail = convert_new_thread_action f nta <-> nta = NewThreadFail"
"convert_new_thread_action f nta = NewThread t x h <-> (∃x'. nta = NewThread t x' h ∧ x = f x')"
"convert_new_thread_action f nta = ThreadExists t <-> nta = ThreadExists t"
"convert_new_thread_action f nta = NewThreadFail <-> nta = NewThreadFail"
by(cases nta, auto)+
lemma convert_new_thread_action_eqI:
"[| !!t x m. nta = NewThread t x m ==> nta' = NewThread t (f x) m;
!!t. nta = ThreadExists t ==> nta' = ThreadExists t;
nta = NewThreadFail ==> nta' = NewThreadFail |]
==> convert_new_thread_action f nta = nta'"
apply(cases nta)
apply auto
done
lemma convert_new_thread_action_compose [simp]:
"convert_new_thread_action f (convert_new_thread_action g ta) = convert_new_thread_action (f o g) ta"
apply(cases ta)
apply(simp_all add: convert_new_thread_action_def)
done
definition convert_extTA :: "('x => 'x') => ('l,'t,'x,'m,'w,'o) thread_action => ('l,'t,'x','m,'w,'o) thread_action"
where "convert_extTA f ta = (\<lbrace>ta\<rbrace>l, map (convert_new_thread_action f) \<lbrace>ta\<rbrace>t, snd (snd ta))"
lemma convert_extTA_simps [simp]:
"convert_extTA f ε = ε"
"\<lbrace>convert_extTA f ta\<rbrace>l = \<lbrace>ta\<rbrace>l"
"\<lbrace>convert_extTA f ta\<rbrace>t = map (convert_new_thread_action f) \<lbrace>ta\<rbrace>t"
"\<lbrace>convert_extTA f ta\<rbrace>c = \<lbrace>ta\<rbrace>c"
"\<lbrace>convert_extTA f ta\<rbrace>w = \<lbrace>ta\<rbrace>w"
"convert_extTA f (las, tas, was, cas) = (las, map (convert_new_thread_action f) tas, was, cas)"
apply(simp_all add: convert_extTA_def)
apply(cases ta, simp)+
done
lemma convert_extTA_eq_conv:
"convert_extTA f ta = ta' <->
\<lbrace>ta\<rbrace>l = \<lbrace>ta'\<rbrace>l ∧ \<lbrace>ta\<rbrace>c = \<lbrace>ta'\<rbrace>c ∧ \<lbrace>ta\<rbrace>w = \<lbrace>ta'\<rbrace>w ∧ \<lbrace>ta\<rbrace>o = \<lbrace>ta'\<rbrace>o ∧ length \<lbrace>ta\<rbrace>t = length \<lbrace>ta'\<rbrace>t ∧
(∀n < length \<lbrace>ta\<rbrace>t. convert_new_thread_action f (\<lbrace>ta\<rbrace>t ! n) = \<lbrace>ta'\<rbrace>t ! n)"
apply(cases ta, cases ta')
apply(auto simp add: convert_extTA_def map_eq_all_nth_conv)
done
lemma convert_extTA_compose [simp]:
"convert_extTA f (convert_extTA g ta) = convert_extTA (f o g) ta"
by(simp add: convert_extTA_def)
lemma obs_a_convert_extTA [simp]: "obs_a (convert_extTA f ta) = obs_a ta"
by(cases ta) simp
types
('l,'t,'x,'m,'w,'o) semantics =
"'x × 'm => ('l,'t,'x,'m,'w,'o option) thread_action => 'x × 'm => bool"
print_translation {*
let
fun tr' [Const ("*", _) $ x1 $ m1,
Const ("fun", _) $
(Const ("*", _) $
(Const ("finfun", _) $ l $ (Const ("list", _) $ Const ("lock_action", _))) $
(Const ("*",_) $ (Const ("list", _) $ (Const ("new_thread_action", _) $ t1 $ x2 $ m2)) $
(Const ("*", _) $ (Const ("list", _) $ (Const ("conditional_action", _) $ t2)) $
(Const ("*", _) $ (Const ("list", _) $ (Const ("wait_set_action", _) $ w)) $
(Const ("option", _) $ o1))))) $
(Const ("fun", _) $ (Const ("*", _) $ x3 $ m3) $ Const ("bool", _))] =
if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3 andalso t1 = t2
then Syntax.const "semantics" $ l $ t1 $ x1 $ m1 $ w $ o1
else raise Match;
in [("fun",tr')]
end
*}
types ('a, 'b) trsys = "'a => 'b => 'a => bool"
types ('a, 'b) bisim = "'a => 'b => bool"
locale trsys =
fixes trsys :: "('s, 'tl) trsys" ("_/ -_->/ _" [50, 0, 50] 60)
begin
abbreviation Trsys :: "('s, 'tl list) trsys" ("_/ -_->*/ _" [50,0,50] 60)
where "!!tl. s -tl->* s' ≡ rtrancl3p trsys s tl s'"
end
end