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

Re: [tlaplus] Re: Fairness in programming languages

On 11/10/21 8:34 AM, Willy Schultz wrote:
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.

Java's ReentrantLock [1] is an example of a synchronization primitive where fairness is exposed to the programmer. By the way, the (fair) lock essentially implements the fairness constraint [2] of a high-level TLA+ spec.


[1] https://docs.oracle.com/cd/E17802_01/j2se/j2se/1.5.0/jcp/beta1/apidiffs/java/util/concurrent/locks/ReentrantLock.html [2] https://github.com/lemmy/BlockingQueue/blob/4fa409b020725631d8fa0fa99ea9c813c3cd40dc/BlockingQueue.tla#L119-L144

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/d61c9c8a-09ed-2875-e196-71270259f974%40lemmster.de.