Skip to content

Add heap_lang lib for "invariant locations": locations with a (pure) invariant attached to them

Ralf Jung requested to merge ralf/gc into master

An "invariant" location is a location that has some invariant about its value attached to it, and that can never be deallocated explicitly by the program. It provides a persistent witness that will always allow reading the location, guaranteeing that the value read will satisfy the invariant.

This is useful for data structures like RDCSS that need to read locations long after their ownership has been passed back to the client, but do not care what it is that they are reading in that case. In that extreme case, the invariant may just be True.

Since invariant locations cannot be deallocated, they only make sense when modelling languages with garbage collection. Note that heap_lang does not actually have explicit dealloaction. However, the proof rules we provide for heap operations currently are conservative in the sense that they do not expose this fact. By making "invariant" locations a separate assertion, we can keep all the other proofs that do not need it conservative.

Edited by Ralf Jung

Merge request reports