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.

[Shane Miller]

My question was not clear.

Suppose one is writing a user or technical guide for TLA. For absolute fairness are there any practical examples one might note?

This question is not about what fairness is or how to choose a fairness flavor ... the question what might are good examples of 

unfair processes? 

As  far as I can see any examples must be few because most software models need weak sometimes strong fairness.

Second, I mentioned SPIN. As you likely know all to well SPIN allows processes to be created in code. This could be important

for motivating practical use of unfair processes. Unfair processes will non-deterministically stop at some point. SPIN can

detect this and run a new copy ... which could be useful to motivate practical examples. But TLA cannot.

Thanks