[teach]

So much this.

I actually did take a formal verification course in college. Our final project was to use the techniques we'd been learning to verify some classic critical-section locking algorithm. I chose to verify an implementation of Lamport's bakery algorithm[0] in C (this was the 90s -- a lot of code was still being written in C).

The problem is that Lamport's algorithm makes an assumption that the "ticket number" is unbounded and any finite implementation in C will almost certainly use a value which is limited to 32 bits or so.

So I was able to formally verify that the algorithm fails to protect the critical section if enough processes are kept waiting to overflow the counter. :)

This probably just means that Lamport's algorithm isn't a great choice for such environments, but I'm still bummed that the professor gave me a B.

[0] https://en.wikipedia.org/wiki/Lamport%27s_bakery_algorithm

[codebje]

You shouldn't have been able to formally verify the algorithm fails to protect the critical section. Wrapping ticket numbers can lead to starvation (literally, if we follow the baker analogy), but the algorithm protects the critical section so long as thread IDs are unique.

The sort of environments in which this is a problem would be extremely uncommon. For a start, you need continuous contention. If you ever get a break in contention you no longer have starvation, and you 'reset' the ticket number monotonicity - to zero, if you actually take a maximum of entering thread ticket numbers instead of a cheap global counter.

If you do actually have an environment in which you expect to have continuous contention over a critical section, some quick napkin math can tell you if it's something to worry about based on the running time of your critical section. If it's over, say, 10ms, you've got a few years of runtime before it's a problem. If it's under 1ms, maybe you want to use 64-bit arithmetic for your ticket number so you can run your system until long after the human species is extinct.

You probably got a 'B' because you didn't give the professor the answer they expected, though, not because of any technical reasons.

[teach]

I'm quite certain I formally verified that two processes were both able to get into the critical section WITH THE ALGORITHM I WAS VERIFYING, but this was 35 years ago, so details are fuzzy.

Remember that this is long before Wikipedia and even before Google, so I have no idea where I'd have gotten the alleged Baker's algorithm from.

Also you're right that this isn't much of an issue in practice, but that's not what formal verification is about, now is it? :)

[codebje]

Formal verification should definitely be about the software you're verifying exhibiting the properties you desire under the conditions you specify.

Formal verification at the undergraduate level, if you even see it, would be about running software on a spherical cow, though.