An introduction to temporal logic and how it can be used to analyze concurrency

> First, let’s prove that a certain protocol ensures that no philosopher will starve. Starvation occurs when a philosopher is perpetually denied access to resources (in this case, forks), and thus can never eat. We'll use a protocol where a philosopher must pick up both forks at once or put down any fork they've picked up and wait before trying again.

This doesn't actually guarantee starvation freedom. Consider a scenario with three philosophers: Plato, Hume, and Arendt. Plato needs forks HA, Hume needs forks PA, etc.

1. Plato picks up forks HA and starts eating.

2. Hume picks up P, fails to pick up A. Hume immediately puts down P and enters the waiting phase.

3. Plato puts down HA.

4. Arendt picks up HP and starts eating.

5. Hume exits waiting phase.

6. Hume picks up A, fails to pick up P. Hume immediately puts down H and enters the waiting phase.

7. GOTO 1

The problem is that there's no guarantee of "strong fairness": that if the system keeps returning to a state where Hume can pick up both forks, he is guaranteed to eventually pick up both forks.

Unrelated, but this is formalism is more precisely known as "linear temporal logic". That's because there are many different temporal logics! Temporal logics are "modal" logics, which means it's a logic equipped with the "necessarily" and "possibly" modifiers. The "necessarily" easily maps onto temporal logic: it just means "true at all times". But what does "possibly" mean?

If I flip a coin, is it "possibly heads?"

In linear temporal logic, the answer is "no", because there are sequences of events where the coin is never heads. In computation tree logic, the answer is "yes", because the timeline has a branch where it lands heads.

Lamport wrote an article arguing that LTL is more useful in the context of programming (https://dl.acm.org/doi/pdf/10.1145/567446.567463). He'd later go on to make TLA, which is a restricted variant of LTL.

I recently started learning about this subject, which is pretty interesting. I had heard about it a while ago, but didn't know much about it besides the basics, and certainly didn't know how it could be applied to real problems since it always seemed pretty abstract. While I did learn about classical logic in college many years ago, I also recently gave myself a refresher on FOL and its axioms and inference rules so I could better understand how temporal logic departs from FOL and builds on it.

Anyway, in an attempt to help me learn the material better, I decided to write up the basic ideas along with several examples of how it could be applied. Perhaps it will be of interest to you as well, although there is certainly nothing new or groundbreaking in my exposition. I did try very hard to make things as simple and concrete as I could while not getting too "hand wavy" as they say.

Caveat: I'm certainly no expert in this field, so if you spot any mistakes, please let me know and I'll revise it (or just submit a PR on GitHub!).

For a more automated way to model and verify concurrency using temporal logic as one tool, see TLA+:

https://en.wikipedia.org/wiki/TLA%2B

That let me think about all the programmers who think, intuitively, that circular buffers with atomic read and write pointers have an easy 'concurrency-safe' proof...

Are there similar systems where the notion of time is not global?

>English: "It is necessary and sufficient for the ground to be wet that it is raining."

That’s not true.

Concurrent algorithms are notoriously hard. There's been tons of academic work to build models/language for concurrency, tools to check properties and so on.

Yet, it seems nothing has emerged that practitioners actually use. I know that there are some occasional experiments (such industrial team specified their protocols using TLA+/Alloy), but it's still extremely limited. I wonder why that is.