1: In this section we turn our attention to the problem of {\em model
2: checking} -- verifying that a given system has certain properties.
3: The property we shall examine in detail is that of deadlock. We give
4: an algorithm for finding a subspace of the state space of a given automaton,
5: such that if the automaton possesses a deadlock~$v$, then the subspace
6: possesses~$v$.
7: In the case of the dining philosophers, this subspace is only quadratically
8: large in the number of philosophers. This result has also been achieved
9: using stubborn sets (see~\cite{valmari:state_art}).
10: We then indicate some examples where the algorithm does not give such
11: a good result. In section~\ref{section:sim_checking}, we shall show
12: how to leverage the algorithm presented here to these cases using
13: abstraction techniques.
14:
15: For the remainder of this section, we restrict attention to finite
16: automata.
17:
18: \subsection{Deadlock detection}
19: \label{section:deadlock_detection}
20:
21: A state~$v$ of a automaton~$S \colon X \to Y$ is said to be a
22: \termdef{deadlock}
23: state if the only motion with source~$v$ is the reflexive motion.
24: For example, if the composite of three dining philosophers and their
25: forks (figure~\ref{fig:phil_3_ring}) is evaluated, the
26: state~$(1,r,1,r,1,r)$ is a reachable deadlock.
27: Naively, to check for a reachable deadlock in an automaton, one must examine
28: every reachable state and determine if it is a deadlock state. In the
29: example of the dining philosophers, a ring of~$n$ philosophers
30: has~$(4 \times 3)^{n}$ states, of which $3^n - 1$ are reachable
31: (for $n \geq 2$).
32:
33: However, we can attempt to exploit the design of the system to simplify
34: our search. The motivating case is the example of products of automata:
35: \begin{proposition}
36: \label{prop:product_deadlock}
37: Let~$S \colon X \to Y$ and~$T \colon Z \to W$ be automata with given
38: initial states~$v_0$ and~$w_0$. If the product~$S \times T$ has a reachable
39: deadlock, then it has a reachable deadlock of the form~$(v^\ast,w^\ast)$
40: where~$v^\ast$ is a deadlock of~$S$ and~$w^\ast$ is a deadlock of~$T$.
41:
42: Moreover, this deadlock is reachable by first considering those motions
43: trivial in~$T$, and then considering those motions trivial in~$S$.
44: \end{proposition}
45:
46: The content of the proposition is that it suffices to check the
47: subautomaton of states of the form~$(v,w_0)$ or~$(v^\ast,w)$ when searching
48: for a reachable deadlock. In general, this subautomaton has a number of
49: states bounded by~$\#S + \#T$, as opposed to the~$\#S \times \#T$ states
50: in the full product~$S \times T$.
51:
52: We define a \termdef{strong deadlock analysis} of an
53: automaton~$S \colon X \to Y$ with initial state~$v$ to be a
54: subautomaton~$T$ of~$S$ such that
55: \begin{enumerate}[(i)]
56: \item $T$ contains~$v$
57: \item If~$w$ is a deadlock state of~$S$ reachable from~$v$,
58: then~$w$ is in~$T$.
59: \end{enumerate}
60: One could also consider the notion of a \termdef{weak deadlock
61: analysis}, where the second condition is replaced by the
62: weaker condition
63: \begin{enumerate}
64: \item[(ii')] If a deadlock state of~$S$ is reachable from~$v$,
65: then~$T$ contains a deadlock reachable from~$v$.
66: \end{enumerate}
67:
68: Then the content of the proposition~\ref{prop:product_deadlock} is that
69: the subautomaton of~$S \times T$ with states those states~$(v,w)$ such
70: that~$v = v^\ast$ or~$w = w_0$, and motions all motions between these
71: states, comprises a weak deadlock analysis of the product. If we include
72: all states~$(v,w)$ such that either~$v$ is a deadlock of~$S$ or~$w = w_0$ we
73: obtain a strong deadlock analysis of the product.
74:
75: \subsection{Introspective Subsystems}
76: \label{section:introspective}
77:
78: Most systems of interest do not decompose as products as required for the
79: deadlock analysis provided by proposition~\ref{prop:product_deadlock} --
80: some coupling is required in order for distributed parts of the system
81: to communicate and achieve a common goal. However, many systems of
82: interest do ``locally decouple'' in the sense that parts do not spend
83: their entire time in communication with each other, and generally restrict
84: their interaction to specific parts of the system at specific times.
85:
86: Before presenting a notion of local decoupling appropriate to our theory,
87: we mention again the example of the dining philosophers. Consider the
88: reachable linearized subautomaton of the binding of a philosopher
89: and a fork as shown in figure~\ref{fig:phil_fork_reachable}. From the
90: state~$(3,l)$ we have a motion to~$(0,u)$ labelled~$(\refl|\refl)$. Being
91: an internal motion of the bound automaton and the only motion out of~$(3,l)$,
92: any behaviour from this state must use this motion, and the environment of
93: the automaton cannot affect the viability of this motion. That is to say,
94: the philosopher and the fork have locally decoupled from the rest of any
95: larger system they may be a part of. We would like to restrict our search
96: for a deadlock by taking advantage of the fact this motion is independent
97: of the action of the rest of the system.
98:
99: Given an automaton~$S$ with boundaries~$(X_i,\mu_i)$, and a state~$v$ of~$S$,
100: we say that~$S$ is \termdef{watching} or \termdef{looking at}
101: boundary~$i$ in state~$v$ if there is a motion~$e \colon v \to w$
102: of~$S$ such that~$\mu_i(e)$ is nontrivial.
103: Conversely, the automaton~$S$ is \termdef{ignoring} boundary~$i$
104: in state~$v$ if every motion with source~$v$ performs the trivial
105: action on the boundary~$X_i$.
106:
107: For example, the philosopher of figure~\ref{fig:phil} is watching the left
108: boundary in states~$0$ and~$2$, and watching the right boundary in states~$1$
109: and~$3$. The fork of figure~\ref{fig:fork} is watching the left boundary
110: in states~$l$ and~$u$, and the right boundary in states~$u$ and~$r$.
111:
112: \begin{proposition}
113: \label{prop:can_move_S}
114: Let~$S \colon X \to Y$ and~$T \colon Y \to Z$ be automata. Let~$v$
115: be a nondeadlock state of~$S$ such that~$S$ is ignoring~$Y$ in
116: state~$v$. For any state~$w$ of~$T$, if there is a
117: behaviour of~$\bind{S}{T}$ with initial state~$(v,w)$ which
118: leads a deadlock~$(v^\ast, w^\ast)$, then
119: there is such a behaviour where the first nontrivial motion is
120: trivial in~$T$.
121: \end{proposition}
122: \begin{proof}
123: Suppose, by way of contradiction, this were not true. Let~$(v,w)$
124: be a state of~$\bind{S}{T}$ such that a deadlock~$(v^\ast, w^\ast)$
125: is reachable from~$(v,w)$,
126: but not by an initial nontrivial motion which is trivial in~$T$.
127: Let~$\beta$ be a behaviour
128: of~$\bind{S}{T}$ with initial state~$(v,w)$ and reaching the deadlock.
129: Write
130: \[
131: \begin{diagram}
132: \beta = (v_0,w_0) & \rTo^{(f_1,g_1)} &
133: (v_1,w_1) & \rTo^{(f_2,g_2)} &
134: (v_2,w_2) & \ldots & (v_n,w_n) = (v^\ast, w^\ast)
135: \end{diagram}
136: \]
137: where~$v_0 = v$ and~$w_0 = w$.
138:
139: We claim some~$f_k$ is a nontrivial motion of~$S$. If not,
140: then~$v_n = v$. Since~$v$ is not a deadlock state of~$S$, there is
141: some motion with source~$v$, say~$e$ labelled~$(x|y)$. Since~$S$ is not looking
142: at~$Y$ in state~$v$, it must be that~$y = \refl$ is trivial. Hence we
143: can extend~$\beta$ with the motion~$e$ in~$S$ and the trivial motion
144: in~$T$, and thus~$\beta$ did not reach a deadlock state, contrary to choice
145: of~$\beta$.
146:
147: Let~$k$ be minimal such that~$f_k$ is a nontrivial motion in~$S$.
148: Note that~$f_i$ is trivial for~$i = 0$,~$\ldots$,~$k-1$. Thus
149: \[
150: v_0 = v_1 = \ldots = v_{k-1}
151: \]
152: The triviality of~$f_i$ for~$i < k$ also implies that the action
153: performed by~$f_i$ on the boundary~$Y$ is trivial. The action performed
154: by~$f_k$ on the boundary~$Y$ is also trivial, since~$S$ is not looking
155: at~$Y$ in state~$v$. Thus, since~$g_i$ synchronizes with~$f_i$, we
156: have that the action performed by~$g_i$ on the boundary~$Y$ is also
157: trivial, for~$i = 0$,~$\ldots$,~$k$.
158:
159: It is now evident that
160: \[
161: \begin{diagram}
162: (v_0,w_0) & = (v_{k-1},w_0) & \rTo^{(f_k,\refl)} &
163: (v_k,w_0) & \rTo^{(\refl,g_1)} &
164: (v_k,w_1) \\
165: \quad & \rTo^{(\refl,g_2)} (v_k,w_2) & \ldots
166: (v_k,w_{k-1}) & \rTo^{(\refl,g_k)} &
167: (v_k,w_k) \\
168: \quad & \rTo^{(f_{k+1},g_{k+1})} &
169: (v_{k+1},w_{k+1}) & \ldots & (v_n,w_n) = (v^\ast, w^\ast)
170: \end{diagram}
171: \]
172: is a behaviour of~$\bind{S}{T}$ with initial state~$(v,w)$
173: that leads to the specified deadlock~$(v^\ast, w^\ast)$,
174: and that has first motion trivial in~$T$. Hence the desired contradiction.
175: \end{proof}
176:
177: For a system with composite automata~$S$ and a global state~$v$ of~$S$,
178: a subsystem is said to be \termdef{introspective at~$v$} if each component
179: of the subsystem, when in the local state corresponding to~$v$, is
180: ignoring every boundary on which it connects to components not in
181: the subsystem.
182:
183: \begin{proposition}
184: \label{prop:introspect}
185: Consider a global state~$v$ of a system and a subsystem that is
186: introspective at~$v$ but not deadlocked when in the local state
187: corresponding to~$v$. If a deadlock of the system is reachable from~$v$,
188: it is reachable via a behaviour whose first nontrivial motion is
189: trivial outside the given subsystem.
190: \end{proposition}
191: \begin{proof}
192: Using the algebra of designs, organize the system as a composite
193: of the given subsystem and its complement:
194: \[
195: \xymatrix
196: {
197: & *+<1.5em>[F-]\txt{Introspective\\Subsystem}
198: \ar@{-}[l]
199: \ar@{-}@<1ex>[r]
200: \ar@{-}[r]
201: \ar@{-}@<-1ex>[r]
202: & *+<1.5em>[F-]\txt{Rest of\\System}
203: \ar@{-}[r] &
204: }
205: \]
206: Now apply proposition~\ref{prop:can_move_S} to the composite of the evaluation
207: of the two subsystems.
208: \end{proof}
209:
210: Given an introspective but not deadlocked subsystem at each global
211: state~$v$ of the composite automata~$S$ of a system, we can apply
212: proposition~\ref{prop:introspect} repeatedly to produce a strong
213: deadlock analysis by including only those motions of~$S$ which are trivial
214: outside the introspective subsystem associated with their source,
215: and including only those states which are reachable from
216: the initial state of~$S$ via the included motions.
217:
218: \subsection{Minimal Introspective Subsystem Analysis}
219: \label{section:misa}
220:
221: It may be that, for a given design, the introspective subsystems are
222: obvious, or designed in to the system so as to provide for
223: more efficient checking. However, it is also desirable to automatically check
224: a given system for absence of deadlock, exploiting the known design
225: of the system to reduce the state space explosion associated with
226: exhaustive model checking.
227:
228: The idea of minimal introspective subsystem analysis is to guide the exploration
229: of the state space via proposition~\ref{prop:introspect}.
230: More precisely, we construct the deadlock analysis
231: of a given system suggested at the end of the the previous section
232: as we explore the state space, by choosing a minimal introspective
233: subsystem at each state.
234:
235: Let us fix for discussion a system with composite automaton~$S$.
236: Given a global state~$v$ of~$S$ and a component of the system,
237: we can examine the automaton assigned to the component to determine
238: which boundaries the automaton is looking at in the local state corresponding
239: to~$v$.
240:
241: Given this information for each component and the design of the
242: system, it is a simple matter to
243: construct a non-deadlocked minimal introspective subsystem at~$v$
244: -- consider the directed graph with vertices the components and edges
245: indicating that the component represented by the source is looking at
246: the component represented by the target, and flood fill along edges from
247: each vertex to find introspective subsystems.
248:
249: This process determines, for each component, the minimal introspective
250: subsystem containing that component. If the global state~$v$ is not
251: a (global) deadlock, then some nontrivial motion is possible. Hence at
252: least one component, and thus the introspective subsystem containing it,
253: is not deadlocked. We select the smallest of these
254: subsystems which is not deadlocked in the local state corresponding to~$v$.
255:
256: We then explore the states of~$S$ only along motions
257: which are trivial outside
258: the selected minimal introspective subsystem, looking for deadlock --
259: proposition~\ref{prop:introspect} guarantees that a reachable deadlock
260: is reachable via a motion trivial outside the introspective subsystem.
261: By maintaining a list of visited states, we can ensure the algorithm
262: terminates.
263:
264: In the event the automata assigned to variables of the design are linear,
265: it suffices to explore the states of~$S$ only along atomic motions
266: (see~\ref{section:atomic}) -- in this case restricting to the subautomaton
267: including only atomic motions does not alter the reachability of states.
268:
269: \subsubsection{Minimal Introspective Subsystem Analysis of Dining Philosophers}
270: \label{section:misa_dp}
271:
272: Let us consider the system consisting of a ring of~$n$ philosophers
273: and their~$n$ intervening forks. Since each automata used in the system
274: is linear, we can restrict our attention to atomic motions.
275: We shall now walk through the application of the minimal introspective
276: subsystem analysis algorithm proposed in section~\ref{section:misa} for
277: this system.
278:
279: Initially, each philosopher is looking at the left boundary, and each
280: fork is looking at both boundaries. So the only introspective
281: subsystem is the entire system, giving~$n$ atomic motions to be explored
282: (each motion being one for which a given philosopher acquires their left
283: fork).
284:
285: Each state reached next has precisely one philosopher having obtained their
286: left fork. Let us consider the state in which the philosopher~$P_1$
287: has acquired his left fork. At this point, we see~$P_1$ is now
288: looking at his right boundary, and~$P_2$ is looking at her left boundary,
289: and the fork~$F_1$ is looking at both boundaries. These three components
290: thus form an introspective subsystem as required. A moments thought
291: shows that it is minimal, and a moments more that it is the only minimal
292: introspective subsystem. There are only two nontrivial atomic
293: motions in this subsystem -- either~$P_1$ acquires the fork or~$P_2$
294: acquires the fork.
295:
296: In the former case, the system comprised of~$P_1$ and his left fork now
297: constitute a minimal introspective subsystem -- the philosopher is
298: in state~$2$ attempting to relinquish the left fork, and the left
299: fork is in state~$r$ having being acquired by the philosopher on its
300: right. The single nontrivial atomic motion of the subsystem is to
301: relinquish the fork. Following this, and by a similar
302: analysis, the philosopher relinquishes his right fork. The system has
303: now returned to the initial state, which is marked as checked.
304:
305: In the latter case of~$P_2$ acquiring the fork~$F_1$, we apply similar
306: reasoning to the competition between~$P_2$ and~$P_3$ to acquire~$F_2$,
307: as these three systems once again comprise the unique minimal
308: introspective subsystem at the global state under consideration.
309: In exploring the case that~$P_2$ is successful, she will
310: proceed to relinquish her left and right forks, and we return to the state
311: where she is competing with~$P_1$. In exploring the case~$P_3$ is successful
312: we examine the subsystem comprised of~$P_3$,~$F_3$ and~$P_4$.
313:
314: The algorithm continues in this manner, obtaining a minimal introspective
315: subsystem comprising two philosophers and their intervening fork at
316: each stage, and progressing in two ways -- allowing one philosopher to run
317: to completion, or moving to the competition for the next fork around the
318: table. Eventually the deadlock in which each philosopher has acquired
319: their left fork is found.
320:
321: It is evident that after the initial state, we explore 3 states for each
322: philosopher (as it moves through states~$1$,~$2$ and~$3$) bar the last.
323: The exploration stops when the last philosopher acquires his left fork,
324: and hence each philosopher has acquired their left fork and the system
325: is deadlocked. Potentially then, we are required to explore the initial
326: state, the final deadlock state, and~$3(n-1)$ for each choice of the
327: initial~$n$ motions. Thus~$3n^2 - 3n + 2$ states are explored, a
328: significant reduction on the~$3^n-1$ reachable states in the system.
329:
330: This result has been described using stubborn sets
331: in~\cite{valmari:error_detect}, where the same polynomial for the number
332: of states checked is computed.
333:
334: \medskip
335:
336: It should be noted that there are systems very similar to the dining
337: philosophers in which the above algorithm does not reduce the checking
338: to a polynomial number of states. Replacing the philosophers by either
339: the system shown in figure~\ref{fig:nondet_phil} or
340: figure~\ref{fig:slow_phil} results in a system for which the above algorithm
341: searches an exponential number of states.
342:
343: \begin{figure}[th]
344: \[
345: \xymatrix
346: {
347: && 1 \ar[lldd]_{(\refl|\lock)}
348: &&&&
349: 1' \ar[rrdd]^{(\refl|\lock)} &&
350: \\ \\
351: 2 \ar[rrdd]_{(\unlock|\refl)}="left"
352: &&&& 0 \ar[lluu]_(0.7){(\lock|\refl)} \ar[rruu]^(0.7){(\lock|\refl)}
353: &&&& 2' \ar[lldd]^{(\unlock|\refl)}="right"
354: \\ \\
355: && 3 \ar[rruu]_(0.3){(\refl|\unlock)}
356: &&&& 3' \ar[lluu]^(0.3){(\refl|\unlock)}
357: &&
358: }
359: \]
360: \caption{\label{fig:nondet_phil} Alternative Philosopher I}
361: \end{figure}
362: The alternative philosopher I, shown in figure~\ref{fig:nondet_phil},
363: may be termed the nondeterministic philosopher. In this case,
364: minimal introspective subsystem analysis of the composite system must check
365: two branches as the minimal introspective subsystem under consideration
366: moves around the table. Informally then, we see that an exponential
367: number of states will be checked (although still significantly less than
368: the total number of states of the system).
369:
370: \begin{figure}[th]
371: \[
372: \xymatrix
373: {
374: 0 \ar[rr]^{(\lock|\refl)}
375: && 1 \ar[rr]^{(\refl|\lock)}
376: && 2 \ar[rr]^{(\unlock|\refl)}
377: && 3 \ar[dd]^{(\refl|\unlock)}
378: \\ \\
379: 7 \ar[uu]^{(\refl|\unlock)}
380: && 6 \ar[ll]^{(\unlock|\refl)}
381: && 5 \ar[ll]^{(\refl|\lock)}
382: && 4 \ar[ll]^{(\lock|\refl)}
383: }
384: \]
385: \caption{\label{fig:slow_phil} Alternative Philosopher II}
386: \end{figure}
387:
388: The alternative philosopher II, shown in figure~\ref{fig:slow_phil},
389: may be termed the double cover philosopher. In this case,
390: when the philosopher returns to the state of wishing to acquire his
391: left fork in the first instance, he is in the local state~4, and not
392: a searched state as in the basic example. Thus the algorithm
393: arrives at many distinct states in which the minimal introspective
394: subsystem is the entire system. There are~$2^n$ reachable
395: global states of this form, and it can be argued that the algorithm
396: proposed above will visit all of them. Informally then we again
397: have a situation where an exponential number of states are checked.
398:
399: It is worth noting that both the nondeterministic and double cover
400: philosophers can be abstracted to the philosopher of figure~\ref{fig:phil}
401: in a sense which is made precise in section~\ref{section:simulations}.
402: This abstraction allows us to use the strong deadlock analysis
403: with only polynomially many states to check the more complex systems
404: (see section~\ref{section:sim_checking}).
405:
406: \bigskip
407:
408: In this section we have outlined the principles of model checking for
409: deadlock as manifested in our theory, and presented a very simple algorithm
410: for reducing state space explosion in model checking. It should be
411: emphasized that although simplistic, the algorithm does have demonstrably
412: good behaviour on a particular system, and importantly exhibits the principle
413: of using design information retained by our calculus to assist in the
414: process of model checking.
415: