Need to be able to justify the analysis and optimisations being applied to the acq_rel automaton. To do this, should identify (or write) a decently-sized piece software that uses locks. Then, apply acq_rel automata in the appropriate places to verify correct behaviour.
While a real piece of software is a good idea, a synthetic benchmark showing performance degradation when dynamically asserting over locks isn't such a bad idea.
Need to be able to justify the analysis and optimisations being applied to the
acq_rel
automaton. To do this, should identify (or write) a decently-sized piece software that uses locks. Then, applyacq_rel
automata in the appropriate places to verify correct behaviour.