1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6chapter \<open>\label{h:abbreviations}Convenience Definitions\<close> 7 8(*<*) 9theory Abbreviations 10imports Types 11begin 12(*>*) 13 14text \<open> 15 This section defines static functionality that the generated glue code 16 semantics relies on. It provides the basic building blocks for the 17 \camkes communication mechanisms. They can also be used as building blocks 18 for users describing the behaviour of trusted components. 19\<close> 20 21subsection \<open>\label{sec:componentlocal}Local Component Operations\<close> 22 23subsubsection \<open>\label{ssec:univc}UNIV$_c$\<close> 24text \<open> 25 The set of all possible states a component can be in. This is 26 essentially any local state with the exception of the states 27 representing events and shared memory. 28\<close> 29definition 30 UNIV\<^sub>c :: "'component_state local_state set" 31where 32 "UNIV\<^sub>c \<equiv> {x. case x of Component _ \<Rightarrow> True | _ \<Rightarrow> False}" 33 34subsubsection \<open>\label{ssec:internal}Internal Step\<close> 35text \<open> 36 An internal step in a component that arbitrarily modifies its own local 37 state. Note that it is not possible for an event or shared memory component 38 to take this step. 39\<close> 40definition 41 internal :: "'component_state local_state \<Rightarrow> 42 'component_state local_state set" 43where 44 "internal s \<equiv> case s of Component _ \<Rightarrow> UNIV\<^sub>c | _ \<Rightarrow> {}" 45 46subsubsection \<open>\label{ssec:userstep}User Steps\<close> 47text \<open> 48 A representation of @{term internal} in the concurrent imperative language. 49 That is, an arbitrary local step. 50\<close> 51definition 52 UserStep :: "('channel, 'component_state) comp" 53where 54 "UserStep \<equiv> LocalOp internal" 55 56subsection \<open>\label{sec:componentcommunication}Communication Component Operations\<close> 57 58subsubsection \<open>\label{ssec:discard}Discard Messages\<close> 59text \<open> 60 Receive a @{term Void} message and do nothing in reaction. 61\<close> 62definition 63 discard :: "'channel answer \<Rightarrow> 'component_state local_state \<Rightarrow> 64 'component_state local_state set" 65where 66 "discard a s \<equiv> if a_data a = Void then {s} else {}" 67 68subsubsection \<open>\label{ssec:arbitraryrequest}Arbitrary Requests\<close> 69text \<open> 70 Non-deterministically send any message on a given channel. This provides a 71 way of specifying unconstrained behaviour of a component given access to a 72 particular channel. The command produces the set of all messages on a given 73 channel as possible questions and receives any response with a fully 74 nondeterministic local state update. 75\<close> 76definition 77 ArbitraryRequest :: "'channel \<Rightarrow> ('channel, 'component_state) comp" 78where 79 "ArbitraryRequest c \<equiv> Request (\<lambda>_. {x. q_channel x = c}) (\<lambda>_ _. UNIV\<^sub>c)" 80 81subsubsection \<open>\label{ssec:arbitraryresponse}Arbitrary Responses\<close> 82text \<open> 83 Non-deterministically receive any message on a given channel. The 84 command receives any message, makes a nondeterministic local state 85 update, and returns the set of all possible responses @{text \<beta>} on 86 the given channel. 87\<close> 88definition 89 ArbitraryResponse :: "'channel \<Rightarrow> ('channel, 'component_state) comp" 90where 91 "ArbitraryResponse c \<equiv> 92 Response (\<lambda>_ _. {(s',\<beta>). s' \<in> UNIV\<^sub>c \<and> a_channel \<beta> = c})" 93 94subsubsection \<open>\label{ssec:eventemit}Event Emit\<close> 95text \<open> 96 Emit an event. The command sends the message @{const Set} on the 97 given channel and discards any response to model asynchronous behaviour 98 with respect to the event buffer components. The message is independent of 99 the local state @{text s}. 100\<close> 101definition 102 EventEmit :: "'channel \<Rightarrow> ('channel, 'component_state) comp" 103where 104 "EventEmit c \<equiv> Request (\<lambda>s. {\<lparr>q_channel = c, q_data = Set\<rparr>}) discard" 105 106subsubsection \<open>\label{ssec:eventpoll}Event Poll\<close> 107text \<open> 108 Poll for a pending event from an asynchronous buffer component. 109 The command sends a @{const Poll} message to the buffer component, and 110 expects a message @{term a} back that has the form @{term "Pending b"} 111 with a boolean payload @{term b}. This payload is embedded in the local 112 state of the component using the user-provided function @{text embed_data}. 113\<close> 114definition 115 EventPoll :: "'channel \<Rightarrow> 116 ('component_state local_state \<Rightarrow> bool \<Rightarrow> 'component_state local_state) \<Rightarrow> 117 ('channel, 'component_state) comp" 118where 119 "EventPoll c embed_data \<equiv> 120 Request (\<lambda>_. {\<lparr>q_channel = c, q_data = Poll\<rparr>}) 121 (\<lambda>a s. case a_data a of Pending b \<Rightarrow> {embed_data s b} | _ \<Rightarrow> {})" 122 123subsubsection \<open>\label{ssec:eventwait}Event Wait\<close> 124text \<open> 125 Wait for a pending event. The command takes 126 a channel @{text c}, and embedding function @{text embed} (see above). 127 Because the set of target states is only non-empty when the pending bit of 128 the polled event is set, this has the effect of blocking the component's 129 execution until the event is available. 130\<close> 131definition 132 EventWait :: "'channel \<Rightarrow> 133 ('component_state local_state \<Rightarrow> bool \<Rightarrow> 'component_state local_state) \<Rightarrow> 134 ('channel, 'component_state) comp" 135where 136 "EventWait c embed_data \<equiv> 137 Request (\<lambda>_. {\<lparr>q_channel = c, q_data = Poll\<rparr>}) 138 (\<lambda>a s. case a_data a of Pending b \<Rightarrow> if b then {embed_data s b} else {} 139 | _ \<Rightarrow> {})" 140 141subsubsection \<open>\label{ssec:memoryread}Memory Read\<close> 142text \<open> 143 Read from a shared memory location. As mentioned above, shared memory is modelled 144 as a separate process in our glue code semantics. The command below issues 145 a @{const Read} request message to this process with a specified address, and expects 146 an immediate response of the form @{term "Value v"} back, which is embedded into 147 the local state with the same mechanism as above. 148\<close> 149definition 150 MemoryRead :: "'channel \<Rightarrow> 151 ('component_state local_state \<Rightarrow> nat) \<Rightarrow> 152 ('component_state local_state \<Rightarrow> variable \<Rightarrow> 'component_state local_state) \<Rightarrow> 153 ('channel, 'component_state) comp" 154where 155 "MemoryRead c addr embed_data \<equiv> 156 Request (\<lambda>s. {\<lparr>q_channel = c, q_data = Read (addr s)\<rparr>}) 157 (\<lambda>a s. case a_data a of Value v \<Rightarrow> {embed_data s v} | _ \<Rightarrow> {})" 158 159subsubsection \<open>\label{ssec:memorywrite}Memory Write\<close> 160text \<open> 161 Write to a shared memory location. The command sends a @{const Write} message to 162 the memory component with specified address and value (which are extracted from the local state) 163 and does not expect a response. 164\<close> 165definition 166 MemoryWrite :: "'channel \<Rightarrow> ('component_state local_state \<Rightarrow> nat) \<Rightarrow> 167 ('component_state local_state \<Rightarrow> variable) \<Rightarrow> 168 ('channel, 'component_state) comp" 169where 170 "MemoryWrite c addr val \<equiv> 171 Request (\<lambda>s. {\<lparr>q_channel = c, q_data = Write (addr s) (val s)\<rparr>}) discard" 172 173text \<open> 174 This concludes the list of the basic operations from which the glue code is 175 composed. We now proceed to 176 define the intermediate communication components for events and shared memory. 177 178\<close> 179(*<*) 180end 181(*>*) 182