Thank you, Markus.I supposed it was mostly kernel level. Also, it's nice to remember about ReentrantLock; I'll read the documentation about it.May I ask in your BlockingQueue spec, why do you need to prove Deadlock freedom in the sense that why is it necessary? Is it good practice to prove specs of its size?Thanks,JonesOn Wed, 10 Nov 2021 at 13:55, Markus Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d61c9c8a-09ed-2875-e196-71270259f974%40lemmster.de.