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.
On Wednesday, November 10, 2021 at 10:45:46 AM UTC-5 jone...@xxxxxxxxx wrote:
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