I’ve ported the Promela algorithm back to Java. The unit tests that I have outside the system all pass, but of course that doesn’t mean anything without a unit testing framework that takes concurrency into account.
Now I’m putting the algorithm into the system, but to make that work, I first have to write the instrumentation strategy that replaces
invokestatic instructions to
setOldThreadwith inlined bytecode, as previously  explained.