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