[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