[Iris-Club] Classical version of Iris?
jung at mpi-sws.org
Tue Aug 16 11:25:43 CEST 2016
> Ralf, Bob, and I have developed a version of Iris based on linear BI in
> our POPL submission. I mean "linear" in the sense that P * Q does not
> necessarily entail P, in contrast to the "affine" set-up in the original
> Iris (I personally find the "intuitionistic"/"classical" separation
> logic terminology confusing).
Same here, for a long time, but I think I now kind of got it... The
model of intuitionistic separation logic (monotone predicates over a
PCM) is a BI, but not a boolean algebra because complement does not
preserve monotonicity. Hence excluded middle does not hold. However,
the model of classical separation logic (predicates over a PCM) is a
boolean algebra, and excluded middle holds (if it holds in the
meta-logic). So, there is some sense to this connection. ;)
> This is part of an extension to Iris that
> we developed for proving fair termination-preserving refinements between
> a source and target language. We have certain resources that represent
> threads of the source program, and in order to make sure that the
> refinement is termination preserving, we needed to precisely track these
> resources and prevent threads from "throwing them away".
One thing I still wonder is whether we can do something more elegant
here, where instead of having a predicate over two resources, we give
more flexibility to CMRAs and allow them to relax the partial order
that's later used for monotonicity... but I'm just rambling here. ;)
> [Later, in reply to Derek's mail]
> Of course, for tracking memory in the setting of partial correctness, what you propose seems like it would work (although I cannot speak to the convenience). Another advantage of what you suggest is that it is easily extended not just to let you track the absence of memory leaks, but also to prove an upper bound on space usage. So, I agree with you that linearity seems like a red herring when it comes to resource usage, at least in the ways it has conventionally been used for that purpose.
I am not sure what "absence of memory leaks" even means in the context
of a concurrent algorithm that involves ownership transfer. In that
sense, I am also not convinced that resources proving absence of
additionally allocated locations will be useful or helpful at all. After
all, concurrently running threads can certainly allocate memory while
this function is running and deallocate it later, so certainly, the
domain of the heap (i.e. the set of allocated locations) can be larger
after calling this function than it was in the beginning.
More information about the Iris-Club