Safety Constraints and Invariants of the Term_ds Module
In the Term_ds term module, type term
has two mutable fields.
Unless the object of type term is used purely internally (i.e. it is created within
some piece of Term_ds code and a reference to it is not
included in any object that may escape that piece of code), the data in mutable fields
of that object may be modified only when the following safety rules are observed:
- Term should look immutable for any code accessing it through the generic term module
- Code should be thread-safe.
In order to observe those rules, we restrict ourselves in the following ways:
We define what it means for a term object to be "valid". This means that
- free_vars field is valid (see rules for calculating free variables)
- if core = Subst (t, ts), then all variables of ts occur in t
and ts does not have the same variable repeated more than once.
We always keep all term objects valid.
We have defined a mapping from valid term objects to terms (Term_std.term objects).
Basically, FOVar "x" maps to variable x, Subst (t, ts) maps to whatever t maps to
with the ts substitution performed, etc. If two term objects map to the same term,
we consider them equivalent.
Whenever we modify the term object in-place, we make sure that the new object is
equivalent to the old one.
For each interface function we make sure that it "respects" term object equivalence.
It is easy to see that (A) and (B) together with (2) guarantee (1).
- The possible values of each mutable field are divided in two categories -
complete and incomplete (delayed).
For free_vars, Vars _ is complete and VarsDelayed is incomplete.
For core, FOVar _, Term _ and Sequent _ are complete and Subst _ is incomplete.
We only change values of mutable fields from incomplete to complete. And for any term
object with incomplete field, only one (w.r.t equivalence) complete value may be
written into that field.
If used correctly, (A-C) would guarantee (2). Indeed, if two threads try to modify
the same field simultaneously, then
- It means that the old values of the field were incomplete in both threads (complete
values can not be modified - C) and since (again C) we never write an incomplete value
into an existing term, the old values must be the same (the one that was there when
that field was created).
- Hence, both threads were trying to write the same (w.r.t equivalence - C) value
into that field, so it does not matter which one succeeded.