Proving What's Possible

<p>As a formal methods consultant I have to mathematically express properties of systems. I generally do this with two "temporal operators": </p> <ul> <li>A(x) means that <code>x</code> is always true. For example, a database table <em>always</em> satisfies all record-level constraints, and a state machine <em>always</em> makes valid transitions between states. If <code>x</code> is a statement about an individual state (as in the database but not state machine example), we further call it an <strong>invariant</strong>.</li> <li>E(x) means that <code>x</code> is "eventually" true, conventionally meaning "guaranteed true at some point in the future". A database transaction <em>eventually</em> completes or rolls back, a state machine <em>eventually</em> reaches the "done" state, etc. </li> </ul> <p>These come from linear temporal logic, which is the mainstream notation for expressing system properties. <sup id="fnref:modal"><a class="footnote-ref" href="#fn:modal">1</a></sup> We like these operators because they elegantly cover <a href="https://www.hillelwayne.com/post/safety-and-liveness/" target="_blank">safety and liveness properties</a>, and because <a href="https://buttondown.com/hillelwayne/archive/formalizing-stability-and-resilience-properties/" target="_blank">we can combine them</a>. <code>A(E(x))</code> means <code>x</code> is true an infinite number of times, while <code>A(x =&gt; E(y)</code> means that <code>x</code> being true guarantees <code>y</code> true in the future. </p> <p>There's a third class of properties, that I will call <em>possibility</em> properties: <code>P(x)</code> is "can x happen in this model"? Is it possible for a table to have more than ten records? Can a state machine transition from "Done" to "Retry", even if it <em>doesn't</em>? Importantly, <code>P(x)</code> does not need to be possible <em>immediately</em>, just at some point in the future. It's possible to lose 100 dollars betting on slot machines, even if you only bet one dollar at a time. If <code>x</code> is a statement about an individual state, we can further call it a <a href="https://en.wikipedia.org/wiki/Reachability" target="_blank"><em>reachability</em> property</a>. I'm going to use the two interchangeably for flow. </p> <p><code>A(P(x))</code> says that <code>x</code> is <em>always</em> possible. No matter what we've done in our system, we can make <code>x</code> happen again. There's no way to do this with just <code>A</code> and <code>E</code>. Other meaningful combinations include:</p> <ul> <li><code>P(A(x))</code>: there is a reachable state from which <code>x</code> is always true.</li> <li><code>A(x =&gt; P(y))</code>: <code>y</code> is possible from any state where <code>x</code> is true.</li> <li><code>E(x &amp;&amp; P(y))</code>: There is always a future state where x is true and y is reachable.</li> <li><code>A(P(x) =&gt; E(x))</code>: If <code>x</code> is ever possible, it will eventually happen.</li> <li><code>E(P(x))</code> and <code>P(E(x))</code> are the same as <code>P(x)</code>.</li> </ul> <p>See the paper <a href="https://dl.acm.org/doi/epdf/10.1145/567446.567463" target="_blank">"Sometime" is sometimes "not never"</a> for a deeper discussion of <code>E</code> and <code>P</code>.</p> <h3>The use case</h3> <p>Possibility properties are "something good <em>can</em> happen", which is generally less useful (<em>in specifications</em>) than "something bad <em>can't</em> happen" (safety) and "something good <em>will</em> happen" (liveness). But it still comes up as an important property! My favorite example:</p> <p><img alt="A guy who can't shut down his computer because system preferences interrupts shutdown" class="newsletter-image" src="https://www.hillelwayne.com/post/safety-and-liveness/img/tweet2.png" /></p> <p>The big use I've found for the idea is as a sense-check that we wrote the spec properly. Say I take the property "A worker in the 'Retry' state eventually leaves that state":</p> <div class="codehilite"><pre><span></span><code>A(state == &#39;Retry&#39; =&gt; E(state != &#39;Retry&#39;)) </code></pre></div> <p>The model checker checks this property and confirms it holds of the spec. Great! Our system is correct! ...Unless the system can never <em>reach</em> the "Retry" state, in which case the expression is trivially true. I need to verify that 'Retry' is reachable, eg <code>P(state == 'Retry')</code>. Notice I can't use <code>E</code> to do this, because I don't want to say "the worker always needs to retry at least once". </p> <h3>It's not supported though</h3> <p>I say "use I've found for <em>the idea</em>" because the main formalisms I use (Alloy and TLA+) don't natively support <code>P</code>. <sup id="fnref:tla"><a class="footnote-ref" href="#fn:tla">2</a></sup> On top of <code>P</code> being less useful than <code>A</code> and <code>E</code>, simple reachability properties are <a href="https://www.hillelwayne.com/post/software-mimicry/" target="_blank">mimickable</a> with A(x). <code>P(x)</code> <em>passes</em> whenever <code>A(!x)</code> <em>fails</em>, meaning I can verify <code>P(state == 'Retry')</code> by testing that <code>A(!(state == 'Retry'))</code> finds a counterexample. We <em>cannot</em> mimic combined operators this way like <code>A(P(x))</code> but those are significantly less common than state-reachability. </p> <p>(Also, refinement doesn't preserve possibility properties, but that's a whole other kettle of worms.)</p> <p>The one that's bitten me a little is that we can't mimic "<code>P(x)</code> from every starting state". "<code>A(!x)</code>" fails if there's at least one path from one starting state that leads to <code>x</code>, but other starting states might not make <code>x</code> possible.</p> <p>I suspect there's also a chicken-and-egg problem here. Since my tools can't verify possibility properties, I'm not used to noticing them in systems. I'd be interested in hearing if anybody works with codebases where possibility properties are important, especially if it's something complex like <code>A(x =&gt; P(y))</code>.</p> <div class="footnote"> <hr /> <ol> <li id="fn:modal"> <p>Instead of <code>A(x)</code>, the literature uses <code>[]x</code> or <code>Gx</code> ("globally x") and instead of <code>E(x)</code> it uses <code>&lt;&gt;x</code> or <code>Fx</code> ("finally x"). I'm using A and E because this isn't teaching material.&#160;<a class="footnote-backref" href="#fnref:modal" title="Jump back to footnote 1 in the text">&#8617;</a></p> </li> <li id="fn:tla"> <p>There's <a href="https://github.com/tlaplus/tlaplus/issues/860" target="_blank">some discussion to add it to TLA+, though</a>.&#160;<a class="footnote-backref" href="#fnref:tla" title="Jump back to footnote 2 in the text">&#8617;</a></p> </li> </ol> </div>