This is a quick implementation of the idea we had a long time ago for exporting our protected invariants into YAML witnesses with ghosts.
protection privatization
For the Freiburg mutex.c example, we essentially generate the same witness with ghosts as the example:
A ghost variable m_locked is declared and updated to match lock and unlock operations of the mutex m.
A flow-insensitive invariant used == 0 || m_locked is generated using the ghost variable.
This is still our special flow_insensitive_invariant because there's the question where one would place the location_invariant when our result in fact holds at every point.
For this example, the result is the same, but one invariant is generated per-mutex with a conjunction for all the protected variables. Also for the relational privatization.
TODO
[x] Add tests using #1357.
[x] Clean ghost variable management up to not be string-based.
[x] What is the right invariant for multiple protecting mutexes?
[x] What to do about ambiguous/unknown mutex lock and unlock operations? When do we have to generate a ghost update to which ghost variable?
Detect ambiguity and give up on those mutexes and globals.
[x] Valid C names for ghost variables, in particular for (alloc@...) locks.
[x] Add ghost variable for multi-threaded mode to avoid needing earlyglobs.
[ ] Prune unused ghost variables.
[x] Are mutex-meet multiple-protecting invariants even right?
[x] Adapt ghost update locations to #1400.
[x] Unlock updates are on wrong node (but lock updates are right)?
[x] e235ba70d1b187a0395f83729ef53f667fc41e6e broke OSX only
[x] Options to disable ghost_variable and ghost_update entry types.
[x] Relational mutex-meet.
[x] Option to output __VERIFIER_atomic invariants unconditionally: they should not be observable anyway, but those ghost updates can be technically tricky to work with.
This is a quick implementation of the idea we had a long time ago for exporting our protected invariants into YAML witnesses with ghosts.
protection privatization
For the Freiburg
mutex.cexample, we essentially generate the same witness with ghosts as the example:m_lockedis declared and updated to match lock and unlock operations of the mutexm.used == 0 || m_lockedis generated using the ghost variable.This is still our special
flow_insensitive_invariantbecause there's the question where one would place thelocation_invariantwhen our result in fact holds at every point.Currently tested only manually with:
mutex-meet privatization
For this example, the result is the same, but one invariant is generated per-mutex with a conjunction for all the protected variables. Also for the relational privatization.
TODO
(alloc@...)locks.earlyglobs.e235ba70d1b187a0395f83729ef53f667fc41e6e broke OSX onlyghost_variableandghost_updateentry types.__VERIFIER_atomicinvariants unconditionally: they should not be observable anyway, but those ghost updates can be technically tricky to work with.