[Iris-Club] Using Iris

[Ralf Jung]

Hi Greg,

> This is an interesting conversation, I'm learning a lot, so thanks.

So am I. :)

>     Ah, that is an interesting approach.  In our case we re-used the same definition
>     of WP and Hoare triples as "normal" (non-CPS) languages, so we likely wouldn't
>     want to derive all the WP laws for this tweaked WP that incorporates an
>     "off" state.
> 
> This particular solution of introducing the "on-off" state is useful for the
> entire system, but it might be solving too restricted of a problem to make
> things clear. Suppose we are trying to implement a threading library that
> exposes "thread_exit" which stops running our thread. We wouldn't want to add a
> state to our system to capture "this thread has ended". At the high level, we
> would formalize threads the way you do in heap_lang, but at the implementation
> level, we would need to make sure that the thread entry point doesn't pop
> anything off the stack because it is the first thing on the stack. Rather, it
> needs to call (probably just a jump to) the "thread_exit" function so that it
> can schedule the next thing. In both cases, a False post-condition (from the
> client point of view) seems appropriate.

I am not sure I am entirely following.  I think we would want to add a state to
our system saying "this thread has ended"; somehow the high-level specification
has to reflect what happens in that case, doesn't it?

>     I could imagine a slightly different take on this though (that also feels more
>     "Irisy" to me): Say we add that state, and we also add a new separation logic
>     assertion you can make about the state saying that it is off. (This would be
>     duplicable because once off, it is off forever.) Then we could make the
>     postcondition of the `halt` continuation say "the machine is off", and also use
>     that as the universal postcondition everywhere. This would only require very
>     local changes to LambdaRust.
> 
> This is reasonable for whole-program termination, though it might be the case
> that folding it into the system actually makes more sense. It might also be that
> you could just define terminal states appropriately in your system and you
> wouldn't need to change anything. 

Currently a terminal state is a value.  I am not sure if adding "any expression
having HALT at evaluation position" as a value would work out so well.
Also, the postcondition of WP is a predicate over the terminal state, so making
"K[HALT]" one of those would still mean we need special treatment that makes
this a different kind of terminal state than the rest of them.

>     I should probably write this down in case we want to change our story there.^^
>     It seems slightly annoying to have to say in every reduction step that also the
>     global "has the machine halted" flag is not set yet, but that's a one-time pain
>     so it's probably not too bad.  (This would likely be easier with a different
>     setup, but the shared Iris definition of WP assumes that there is a pool of
>     threads which all carry some per-thread state [for us, that's the expression,
>     the code still to be run there -- because we are using substitution, there are
>     no environments] and then some global state [the heap, usually].  Halting is a
>     clearly a cross-thread concern, but we only define a per-thread reduction which
>     is the automatically lifted to a thread pool.  So we would add a flag in the
>     global state to reflect whether the machine has halted, and not allow any
>     further per-thread reductions after that happened.  We could of course also
>     decide not to use the shared WP, define our own, and still benefit from most of
>     the Iris machinery [the proof mode and invariants and all that would still just
>     work], but we usually try to avoid that.)
> 
> Just to throw one other thing on the table about code-pointers and Hoare
> doubles. I like the uniformity that code-pointers provide for control flow
> operators in languages such as C. For example, VST has 4 possible
> post-conditions (normal termination, doing a 'return', doing a 'break', and
> doing a 'continue'). If you reflect all these simply as function pointers, then
> you don't need any fundamental support in your logic for this sort of
> multiple-return types. 

Yeah, that's one reason we used lambda-terms for this in lambdaRust: If we ever
want to add support for `panic!` (which Rust's form of unwinding, like C++
exceptions), then that'd just be another continuation.  It wouldn't be special
in the operational semantics at all.

> When I say "invariant" here, I am thinking of the base definition of invariant
> without any nice reasoning principles on top of it. For example, for any system
> described by (s0, step), you have s is an invariant (I) if `forall s, step^* s0
> s -> I s`. From the thread-local invariants (which are dependent on the
> permissions of each thread and the pc of the thread) we construct I by saying
> something like "the assertions of all threads can be starred together". While I
> don't have the deepest understanding of how Iris invariants work, I would assume
> that they fit into this somehow, otherwise WP would be difficult to prove sound.

Ah, so that would be the induction hypothesis maintained by the WP soundness
proof.  The setup is slightly different because WP is a separation logic
assertion that can own something.  Basically, if the current program state is

  ([e_0, ..., e_n], \sigma)  ( thread pool of expressions, and shared state )

and the final postcondition is Q, then the invariant is the following separation
logic assertion (we are doing this induction, the WP soundness proof, inside Iris):

  world \sigma * WP e_0 {{ Q }} * WP e_1 {{ True }} * ... * WP e_n {{ True }}

where "world \sigma" is "World satisfaction", which says that all the invariants
that have been allocated so far hold (new invariants can be allocated any time).
 "Hold" here really means "we own the resources to justify them", and they are
of course starred together.  There's also a "state interpretation" predicate
supplied by whoever instantiate the language with Iris, which translate the
shared state \sigma into an iris assertion (usually about owning some ghost
state that is hence kept in sync with the physical state).  It's like another
invariant, that connects the physical state to everything else.
  Notably, Iris assertions are *not* predicates over the physical state of the
machine, as is usually the case in separation logic.  They are predicates over
the ghost state; the physical state comes in later and we use Iris' flexible
ghost state to obtain the usual \mapsto predicate.  Thinking in terms of
"fiction of separation", in Iris even the separation provided by \mapsto is
fictional.  It is no more or less "real" than providing a fiction of
\mapsto-with-fractions on top of a basic \mapsto. The Iris base logic doesn't
even have a notion of a program state, so this is really the only way we can set
these things up.

All of that said, this setup puts enough layers of abstraction between what
users work with (Iris invariants) and the WP induction hypothesis that I have a
hard time translating statements referring to the PC back into the Iris world --
at least thinking in terms of a language like heap_lang, where the "PC" really
is just a lambda term that still needs to be reduced.

Kind regards,
Ralf