[Iris-Club] Using Iris

Gregory Malecha gmalecha at gmail.com
Fri Sep 21 22:54:30 CEST 2018


Hi, Joseph --

Thanks for the response.

On Fri, Sep 21, 2018 at 3:01 PM Joseph Tassarotti <jtassaro at andrew.cmu.edu>
wrote:

> 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?
>
This is a good point. I would have thought to use False rather than True in
the post-condition, is there a reason that you chose False?

>
>
>> 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.
>
Unfortunately, we have a lot of different protocols, so baking it into the
language probably won't work.

>
> 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'll take a look at the paper, it sounds like it would be useful.

>
> 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).
>
Sounds great, it would be great to chat. I'm down in Kendall Sq.

>
> 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
>>
> --
> 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
>


-- 
gregory malecha
gmalecha.github.io
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20180921/cae25381/attachment-0001.html>


More information about the Iris-Club mailing list