[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Fairness in programming languages

Typically, whether or not liveness is ensured (i.e. via fairness) for a multi-threaded concurrent program (e.g. in C++) may be dependent on the policy of the OS scheduler. It may also, for example, be dependent on the scheduling/queuing policy implemented in the synchronization primitives you use (e.g. locks, condition variables, etc.). In general, though, I usually consider such fairness concerns in real world concurrent programs as things that are "under the hood" e.g. at the OS kernel level. 

This might vary from instance to instance, though. For example, if you have a program where threads are scheduled in user space, you may have more fine grained control over the scheduling policies. Also, in a distributed system, where separate programs are operating concurrently, fairness assumptions for each process may also become more explicit and/or controllable e.g. "if a process is non-faulty for long enough and has a message in its queue then it will eventually process the message" or something like that.

On Wednesday, November 10, 2021 at 10:45:46 AM UTC-5 jone...@xxxxxxxxx wrote:
Hello everyone,

Maybe I'm asking the wrong question or thinking in the wrong way.

When specifying a system in TLA⁺, it's useful to describe if certain actions are strongly fair, weakly fair or not fair at all, so that we can verify temporal properties with TLC. When implementing such a system with a programming language, how would we go about implementing these fairness requirements? Is fairness something our implementation does by itself, so we don't need to mention it at all? Is fairness defined in the kernel? Etc.

Best regards,

Jones Martins

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4536a16f-dbdc-4b48-9f54-bfd8df795193n%40googlegroups.com.