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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/4bAoiI44xGY/unsubscribe.
To unsubscribe from this group and all its topics, 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.