[Iris-Club] Comparison of Iris and FCSL

[Gregory Malecha]

Hi, Ralf --

Thanks for the very helpful comparison.

On Wed, Jan 9, 2019 at 8:16 AM Ralf Jung <jung at mpi-sws.org> wrote:

> Hi,
>
> > Does anyone on the list have a good understanding of FCSL to give a
> high-level
> > comparison of the systems (and their relative strengths)? When I last
> looked at
> > FCSL I had the take-away that it built around PCMs which, in my
> understanding,
> > is similar to Iris, but from a discussion that I had today, it seems
> there might
> > be some fundamental differences.
>
> I could probably go on for quite a while about this, but here's the short
> version.  Also this is obviously somewhat biased; I'll do my best to fairly
> represent FCSL, including the design choices I do not agree with. ;)
>
> Yes, FCSL also is "built around" PCMs to some extend.  However, FCSL
> combines
> PCMs with a built-in notion of state-transition systems and an
> interpretation
> function from the states of that STS to the PCM (they call all of this
> together
> a "concurroid").  The STS describes how the resources defined by the PCM
> can be
> moved around and updated.  In contrast to that, Iris uses *just* PCMs --
> well,
> resources algebras (or CMRAs if you also want some step-indexing in your
> resources, but in the vast majority of cases you don't), but nothing like
> STSs.
>  You can of course reason with STSs in Iris, by using an encoding in terms
> of
> PCMs.  But from a user perspective, I don't think this makes much of a
> difference.
>
> The most fundamental difference is around the expressive power of
> invariants:
> Iris' invariants are "semantic", they are impredicative and can be
> "hidden",
> while FCSL invariants are "syntactic" and cannot be hidden.  So, in FCSL,
> the
> Hoare triple has the form "{ P } e { Q } @ Invariant", meaning you
> syntactically
> have to state the invariant(s) under which the triples is verified.  The
> only
> form of hiding that is possible here is if the invariant is strictly
> confined to
> `e`, where `e` initially establishes the invariant based on `P` (and
> resources
> it might have allocated) and then releases all resources captured by that
> invariant before terminating, then it can be "framed away".  Iris supports
> that
> pattern with "cancellable invariants".  However, once you look at
> higher-order
> code that returns a closure, then if that code relies on an invariant
> established by the function that created the closure, in FCSL you have to
> expose
> that invariant to your clients, while in Iris the Hoare triple "{ P } e {
> Q }"
> can just implicitly use all invariants that have already been established,
> without leaking their existence to the client.
> For example, something like the example in §2 of [5] cannot be done in
> FCSL.
>
> [5]: https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf
>
> On a related note, FCSL's model of concurrency is weaker than the one in
> Iris:
> FCSL uses fork-join concurrency, meaning the only way to spawn a thread is
> parallel composition.  After "e" reduced to a value, we know that also all
> the
> threads it spawned have terminated again.  (This is required for soundness
> of
> the "invariant framing" I mentioned above.)  In Iris, we use the more
> general
> fork-based concurrency, where you can fork off a thread with some arbitrary
> computation, and the original thread just keeps going independently.  Of
> course
> one can implement parallel composition on top of that, and it is
> straight-forward in Iris to prove the expected specification for that [3].
>
> [3]:
>
> https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lib/spawn.v
> ,
>
> https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lib/par.v
>
> Moreover, invariants in FCSL are somewhat "first-order" -- to specify, for
> example, a spin-lock, you cannot just quantify over whatever invariant the
> client wants to have guarded by the lock.  Instead, the concurroid
> specifying
> the spin lock has some "lose ends" in its STS which a client can "connect"
> to,
> with transitions that are taken when a lock is acquired/released.  This
> can be
> used to transfer resources between the client and the library.  I'm afraid
> I
> don't have a very deep understanding of how this works in FCSL, I never
> understood this part very well.  But I think it is a consequence of this
> difference that a spin lock in Iris takes less than 100 lines to verify [1]
> while it's around 1200 lines in FCSL [2] (but their number is from 2015,
> it is
> possible that they have improved since then).
> For other data structures the amount of code required is much more
> comparable,
> so I think this is related to the fact that ownership transfer of arbitrary
> (client-defined) resources is much harder to express in FCSL than in Iris.
> Iris
> can do this because its invariants are impredicative.  By making this
> choice,
> FCSL can get away with a much simpler model and without step-indexing, and
> indeed they do their reasoning inside the model directly, which would be
> infeasible in Iris.  Iris is only usable in Coq thanks to the MoSeL proof
> mode
> (formerly IPM).
>
> [1]:
>
> https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/lib/spin_lock.v
> [2]: https://ilyasergey.net/papers/fcsl-pldi15.pdf
>
> In FCSL, you can make direct statements about the resources of the "other"
> party, meaning the resources everyone else owns.  In Iris, you can get a
> similar
> effect by using the auth construction, which we use a lot.  We do not have
> a
> general encoding of "other"-based reasoning into Iris, but we have found
> auth to
> be always sufficient.  Using "other" can lead to more direct statements
> (Iris
> proofs tend to have indirections through the ghost state a lot the moment
> you
> need to bound interference, and the bookkeeping takes some getting used
> to), but
> on the other hand, Iris does not have to deal with reasoning about
> "stability":
>  In FCSL, you have to always make sure (and prove, when working in Coq)
> that the
> statements you are making are stable under interference from other threads
> --
> using the "other", you can say things that are true right now but might
> stop
> being true when another thread takes a step.  In Iris, all assertions are
> stable, so you never have to worry about this.
>
> FCSL is based on Hoare Type Theory, so the programs FCSL reasons about are
> actually Coq terms (in some monad for the effects).  That's great for
> reasoning
> about algorithms as you can just use Coq's computational expressiveness,
> and
> your terms even compute during reasoning -- you get conditionals and
> pattern
> matching and so on for free.  Iris relies on a deep embedding of the
> programming
> language with a small-step semantics, meaning there's much more legwork to
> be
> done to get a basic language to reason about (we did much of that with
> heap_lang, included in Iris).  But this also means that you can define
> your own
> deeply embedded language and use it with Iris, as has been done several
> times,
> while AFAIK FCSL has not been related to a small-step semantics yet (but
> that
> might well be possible with the right monad).
>
> By avoiding step-indexing, FCSL can be used directly to reason about
> liveness
> properties.  In particular, FCSL is a linear separation logic and always
> proves
> absence of memory leaks.  Doing the same in Iris is much more complicated
> [4],
> and might not be possible at all for some other liveness properties.  Doing
> liveness reasoning along the lines of Total-TaDA [6] in a step-indexed
> logic
> remains an open problem.
>
> [4]: https://iris-project.org/pdfs/2019-popl-iron-final.pdf
> [6]:
>
> https://www.doc.ic.ac.uk/~pmd09/research/publications/2016/esop/modular-termination-verification-for-non-blocking-concurrency.pdf
>
> I think these are the most important points, let me know if there are any
> questions!
> Kind regards,
> Ralf
>


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