20: Obligations and The Past

tags: `Tag(sp22)`

The first Electrum-mode homework is out! Ask questions early, and we'll try to answer or clarify as needed.
Remember the definition of "configuration": the value of all relations that aren't marked var. Thus, if you click the Sterling button that asks for a new configuration, the solver will always find a new trace that varies on one or more of those relations.
TA applications are open, and close on Wednesday!
The Electrum lab is/was the last formal lab. We'll have "col-labs" for some projects, but they won't be new deliverables to check off.
Final-project presentations will be roughly from May 13th through May 18th–-if you need to travel, and prefer to present earlier, early slots are possible. These are likely to be over Zoom, and public.
Our official finals date is the 17th, so I suggest graduating seniors try to get slots before that, so I can get your grades in on time.

Looking ahead, we'll spend a couple more days on LTL (at least). One of those days, I want to model the temporal logic in the same way we modeled boolean logic, so we can play with the definitions.

After that, we'll start talking technically about how Forge works. Many of you have been curious, and it will set you up well for the homework after Spring break, where you'll be building your own solver.

Back to LTL: Obligation

The until operator can be used to express a stronger sort of eventually. If I write stopped until green_light, it means two things:

the light eventually turns green; and
the stopped predicate holds until the light turns green.

This operator is a great way to phrase obligations in properties and constraints.

Some logics include a "weak" until operator that doesn't actually enforce that the right-hand side ever holds, and so the left-hand side can just be true forever. But, for consistency with industrial languages, Forge's until is "strong", so it requires the right-hand side hold eventually.

Priming: "next state" expressions

You can talk about the value of an expression in the next state by appending ' to the expression. So writing flags' means the value of the flags relation in the state after this one.

The Past (Rarely Used, but Sometimes Useful)

You won't need to use this often, but Forge also includes temporal operators corresponding to the past. E.g., you can say:

prev_state init

to mean that the previous state satisfied the initial-state predicate. But beware: traces are infinite in the forward direction, but not infinite in the backward direction. For any subformula F, prev_state F is false if the current state is the first state of the trace.

There are also analogues to always and eventually in the past: historically and once.

You've seen some of these in lab, or in the documentation that the lab refers you to. We won't use all these operators in 1710.

Modeling Deadlock

A deadlock state is one where no outgoing transitions are possible. How can we write a test in temporal mode that tries to find a reachable deadlock state? There are two challenges:

How do we phrase the constraint, in terms of the transition predicates we have to work with?
How do we even allow Forge to find a deadlock, given that temporal mode only ever finds lasso traces? (A deadlock in a lasso trace is impossible, since a deadlock prevents progress!)

Let's solve the second challenge first, since it's more foundational.

Finding Deadlocks Via Lassos

We could prevent this issue by allowing a doNothing transition from every state. Then from Forge's perspective there's no "deadlock", and a lasso trace can be found.

But this fix causes new problems. If we allow a doNothing transition to happen anywhere, our liveness property is definitely destroyed, even if we were modeling a smarter algorithm. So we need to reduce the power of doNothing somehow.

Put another way: we started with an overconstraint bug: if only lassos can be found, then we can't find a trace exhibiting deadlock. Adding doNothing fixes the overconstraint but adds a new underconstraint, because we'll get a lot of garbage traces where the system can just pause arbitrarily (while the trace continues).

We'll figure out how to fix this next time.