Fairness in programming languages

[Jones Martins]

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

[Willy Schultz]

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.

Will

[Markus Kuppe]

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

[Jones Martins]

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,

Jones

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d61c9c8a-09ed-2875-e196-71270259f974%40lemmster.de.

[Jones Martins]

Thank you, Markus AND William. Sorry.

Best regards,

Jones

[Markus Kuppe]

On 11/10/21 2:00 PM, Jones Martins wrote:
> 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?

In the BlockingQueue spec, the prove serves mainly as an illustration of
TLAPS. However, it still proves that the algorithm is deadlock-free for
*any positive number* of processes. In contrast, model-checking only
proves that the algorithm works for a particular, finite number of
processes.

TLA+ specs are usually small (up to ~2k LOC), yet it is still worth
writing a proof for some of them (think Paxos). Also, contrast, e.g.,
the size of the spec and the proof [2] of a non-blocking algorithm for
process renaming [1].

Markus

[1] http://pardi.enseeiht.fr/Papers/TAP2019.pdf
[2] http://hurault.perso.enseeiht.fr/RenamingProof/Renaming.tla

[Jones Martins]

Wow, that is one large proof.

Am I right in assuming that, depending on the scale of the algorithm (I'm thinking “planetary scale”), it's important to prove instead of only model check an algorithm? Model checking, say, Paxos with thousands of processes, even with dozens of workers, will take months to finish. Putting some effort into proving the algorithm, thus, is critical to ensure correctness of large-scale implementations?

Jones

[Leslie Lamport]

You may want to use a sorting algorithm to sort millions of elements.  I defy you to find a sorting algorithm that correctly sorts any 4 elements but incorrectly sorts a million elements--without writing something like "if N =< 4 then ...".  The same applies to millions of processes.  The problems that depend on scale are performance problems, not correctness problems.  For particular performance problems, there are things one can try to do.  For example, you can try to verify an upper bound on the number of messages taken to do something as a function of the number of processes.  But as far as I know, that is generally done in industry by informal reasoning and testing, and it is not effective at finding rare problems.

Leslie

[Jones Martins]

Thank you, Mr. Lamport. It's clear to me now. I added proving algorithms in TLA⁺ as my next objective.

Best regards,

Jones