[tlaplus] Re: Specifying Garbage Collection

I suppose I need to repeat this advice on how to write a spec every
few years. Your spec is going to represent an execution of the system
and its environment as a sequence of atomic actions/operations. Write
down (the beginnings of) one or three such sequences. Next choose a
set of variables such that each of those actions/operations is
uniquely described as a step--a change to the values of those
variables. Each of those sequences can then be written as a sequence
of states (assignments of values to variables). You will then have to
describe the set of sequences of states that represent correct
executions of the system and its environment by an initial-state
predicate and a next-state relation. In doing so, you may need
additional variables. (For example, if a state-change is enabled by
something that happened in the past, then you may need to add a
variable whose value tells you whether or not that thing happened.)

To express liveness, you could conceivably have to add more variables.
However, that's hardly ever necessary. Learning to express liveness
properties requires reading liveness specs others have written and
practice writing your own. For example, requiring that any item of
garbage is eventually collected can probably be expressed as fairness
of the action that collects an item, since that action should be

enabled if and only if the item is garbage.

Leslie

On Sunday, July 28, 2019 at 9:20:57 AM UTC-7, dominik wrote:

Hello,

I'm trying to model a Garbage Collector. I have a set of objects
Objects
and a predicate
Collectible(Objects, Object) ⟶ True

If the predicate Collectible yields True, the object may be collected by the Garbage Collector.

The safety property of the Garbage Collector shall state, that no object may ever be deleted by the Garbage Collector if the object is not collectible i.e. Collectible yields False.

The liveness property of the Garbage Collector shall state, that every object that is forever collectible i.e. Collectible yields True that object has to eventually be deleted by the Garbage Collector.

Objects can be deleted by other actors whether Collectible yields True or False. So the "origin" of a delete is relevant.

I am not sure how to specify this correctly. Should I introduce helper variables that record the actor, the action taken, and the object? Also, the liveness property is challenging: As soon as an object is deleted, that object is not collectible any more, it has already been collected, so the "forever collectible" seems hard to express.

Thanks for your help!