[Iris-Club] Comparison of Iris and FCSL

[Ralf Jung]

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