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