[Iris-Club] Classical version of Iris?

Joseph Tassarotti jtassaro at andrew.cmu.edu
Tue Aug 16 21:16:42 CEST 2016


On 08/16/2016 05:25 AM, Ralf Jung wrote:
>
> 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. ;)

Right, my objection is just that whether (1) excluded middle and (2) P * 
Q |- P hold are a-priori separate issues. It just so happens that in the 
standard model, if it's non-monotone, you validate (1) and not (2), and 
the monotone version gives you the opposite, but I don't see 
fundamentally why they're linked. And for purposes of tracking memory 
leaks, it's (2) that's relevant, not excluded middle. So, the 
terminology is not wrong per-se, but its used in a way that leads people 
to conflate these two things.

> ...
> 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.

Right, if your concurrency primitive is forking, then it's not clear 
what it means, because you similarly "hide" resources by passing them to 
a child that never deallocates them. I think what becomes more important 
is just knowing that there is some sort of overall upper bound on memory 
usage -- for which you want to use the resource-bound ideas of Jan 
Hoffmann and his collaborators, which I think can be encoded just fine 
in an affine setting.

-Joe




More information about the Iris-Club mailing list