<div dir="ltr">Hi, Joseph --<div><br></div><div>Thanks for the response.<br><br><div class="gmail_quote"><div dir="ltr">On Fri, Sep 21, 2018 at 3:01 PM Joseph Tassarotti <<a href="mailto:jtassaro@andrew.cmu.edu">jtassaro@andrew.cmu.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div>Hi Gregory,</div><div dir="ltr"><br></div><div dir="ltr">On Wed, Sep 19, 2018 at 3:01 PM Gregory Malecha <<a href="mailto:gmalecha@gmail.com" target="_blank">gmalecha@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr">Hello --<div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div></div></div></blockquote><div><br></div><div>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?</div></div></div></blockquote><div>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? </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div></div><div>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?</div></div></div></blockquote><div><br></div><div>There are a couple of things you can do, depending on what notion of "adherence" to a protocol you want to enforce.</div><div><br></div><div>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.</div></div></div></blockquote><div>Unfortunately, we have a lot of different protocols, so baking it into the language probably won't work. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div><br></div><div>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.</div></div></div></blockquote><div>I'll take a look at the paper, it sounds like it would be useful.</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div><br></div><div>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.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div><br></div><div>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.</div><div><br></div></div></div></blockquote><div><br></div><div>I would be happy to chat about it more, and I live in Boston (though I'm traveling a bit at the moment).</div></div></div></blockquote><div>Sounds great, it would be great to chat. I'm down in Kendall Sq. </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div><br></div><div>Cheers,</div><div>Joe </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div></div><div>Thanks for any feedback.</div><div><div><br></div>-- <br><div dir="ltr" class="m_-967602937299062623m_7318653596230663663m_2294560266436205366gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="https://gmalecha.github.io" target="_blank">gmalecha.github.io</a></div></div></div></div></div></div></div></div>
-- <br>
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mpi-sws.org</a><br>
</blockquote></div></div>
-- <br>
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mpi-sws.org</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="https://gmalecha.github.io" target="_blank">gmalecha.github.io</a></div></div></div></div></div></div></div>