Re: [tlaplus] Re: Fairness in programming languages

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.

Markus

[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.