[Iris-Club] Using Iris

[Joseph Tassarotti]

Hi Gregory,

On Wed, Sep 19, 2018 at 3:01 PM Gregory Malecha <gmalecha at gmail.com> wrote:

> Hello --
>
> I'm interested in using Iris in a large (industry) development and I have
> a few questions about it to see if it is something that would work for us.
> Two questions come to mind right now, but more will probably come up as I
> dig deeper.
>
> 1/ All of the resources that I have seen have applied Iris to Hoare
> triples. Has anyone tried applying it to Hoare doubles, i.e. `{ P } c`
> means that `P` guarantees that `c` is safe (but says nothing about a final
> state). I thought that the RustBelt work might have done something like
> this since the paper talks about how the logic is applied to a CPS language
> but I didn't find anything in that development.
>
>
What about just considering triples of the form { P } c {x. True}? This
ensures that c is safe, so I think it suffices for what you want, right?


> 2/ One of the things that I need to track in the development is
> interactions with the outside world (for our project, this is hardware like
> ethernet nics). Right now, I'm thinking that a nice way to do this would be
> through a pre-condition that states what traces are possible when running
> the program. Essentially, I want to add a spatial predicate `TRACE p` such
> that `{ TRACE p } c` means that the only interaction that `c` can do is to
> follow the protocol defined by `p` which is morally something akin to
> `trace -> Prop`. My intuition suggests that this should be fairly simple in
> Iris if I model it as a module that carries around the trace behind an
> abstract predicate. The difficulty is that I need to ensure totality,
> mainly that I have to follow the protocol, i.e. I can't diverge. Normally,
> this would just require a total Hoare logic, but if my protocol is
> infinite, things become a little more complex. Has anyone done something
> like this before? Is there anything that I should be weary of?
>

There are a couple of things you can do, depending on what notion of
"adherence" to a protocol you want to enforce.

a) If you are interested in a kind of safety property (all steps taken are
valid according to the protocol), and the protocols mostly have to do with
interacting with hardware in a certain fashion, then you can just augment
the operational semantics of your language in a way which tracks the state
of the program-hardware interaction, and which gets stuck if you violate
the protocol. Then, the normal soundness theorem for Iris will guarantee
that if you prove a triple {P} c {x. Q}, the program c does not get stuck.
This safety guarantee applies even if c has a diverging execution. If this
suffices for what you need, I would advise doing this.

b) If instead you want to establish a kind of liveness property, or you
want to prove that different programs implement/follow rather different
protocols, then something more along the lines of what you sketched is
appropriate, where the protocol is represented as a resource. Ralf, Bob,
and I consider something like this in the context of Iris in our ESOP 2017
paper, adapting earlier ideas of Atkey, Hoffmann and others. The idea is
that you can modify the definition of weakest precondition in Iris to
ensure that any time the program takes a step, one is also obliged to show
that a "step" of the protocol can be simulated (by updating the resource in
a suitable way).  If the protocol is finitely branching (i.e. if you are in
some state s, the set of states s' you can advance to in a single step from
s is finite), then one can argue (classically) that if the program has a
diverging execution, there is an infinite sequence of steps permitted by
the protocol. So, if the protocol has no such infinite executions, the
program must terminate. The condition on finite branching is a little
annoying, but it arises because of the fact that the Iris model uses step
indexing.

I would not necessarily advise directly using the logic from our paper,
because there's some extra complexity there because we wanted to consider a
notion of fair scheduling which may or may not be applicable in your
situation.


>
> I'd be interested in chatting more with anyone if they have an hour or so,
> I am in Boston and have a relatively flexible schedule to accommodate other
> time zones.
>
>
I would be happy to chat about it more, and I live in Boston (though I'm
traveling a bit at the moment).

Cheers,
Joe


> Thanks for any feedback.
>
> --
> gregory malecha
> gmalecha.github.io
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20180921/5bff9e08/attachment.html>