Practical applications of absolute fairness in software models?

[Shane Miller]

Most models for software or CSP (concurrent sequential processes) use weak fairness with sporadic use of strong.

Are there examples perhaps for niche problems where unfair (absolute) processes is useful?

Other model checkers (eg. SPIN) allow processes can be created at will in code. TLA doesn't seem to do this. So TLA usage here, if it exists, must surely be for single-shot use?

Regards

[Stephan Merz]

Deciding what fairness conditions it is reasonable to assume requires experience. A typical example of specifications where you do not want to require fairness for some of the actions are overlay algorithms, such as termination detection [1]: here one needs to describe "environment" transitions that represent actions of the underlying algorithm, but typically one wants to impose fairness conditions only on actions of the overlay (termination detection) algorithm.

I am not sure I follow your argument about Spin vs. TLC: both are finite-state model checkers, so you will have to bound the number of processes that execute. In TLA+, you typically declare a constant that represents the set of overall process IDs, and a process may very well start when other processes have already executed. In fact, you may define an action that represents process creation. For model checking with TLC, you will have to bound the state space, either by making the action that spawns a new process fail when no process ID is available or, more elegantly, by imposing a state constraint that bounds the number of executing processes that TLC considers.

Stephan

[1] see e.g. https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840.tla for a concrete example

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4e3f4ee6-5696-454c-a5a5-bd2d362732fen%40googlegroups.com.