Ben-Or: Checking liveness properties

[ghost]

I am trying to implement Ben-Or's algorithm and test it for safety and liveness. I'm using the UnReliableBroadCast, FailureInjector and Timer provided by the tutorials. If I make fail less than N/2 processes, and no matter how much I increase the temperature-threshold or the max step, the protocol does not make progress. Ben-Or is a probabilistic algorithm that should terminate with probability 1. I always see the following error that I assume is the liveness check:

<StrategyLog> Found bug using 'random' strategy.
Error: PImplementation.Progress detected potential liveness bug in hot state 'PendingReqs'

When I replace the unreliable broadcast with the reliable one it clearly works. I tried to check the Paxos tutorial that looks similar respecting to the network assumptions, but it does not compile.

Is it reasonable what is happening? How many steps should I allow for seeing progress? Also, is the "cold" state modifier still needed or only the "hot"?

This is my Ben-Or implementation: https://github.com/pinzaghi/themiscyra/blob/master/examples/P/BenOr/PSrc/BenOr.p and the liveness spec: https://github.com/pinzaghi/themiscyra/blob/master/examples/P/BenOr/PSpec/Progress.p

EDIT: Looking in detail the logs, I found something strange. For some reason the cancel timer function do this:

fun CancelTimer(timer: Timer)
{
  send timer, eCancelTimer;
  receive {
    case eTimeOut: {}
  }
}

and my process blocks forever waiting for the eTimeOut event. Why is this implemented this way? Why should I wait for an event after canceling a timer?

[ankushdesai]

Hi Ben,

The timer machine has been edited in the latest commit and final version of the tutorials. Can I please request you to update your models to use the latest version of the time, failure detector and injector?

After you have done that, I agree with you that if the Ben-Or algorithm must always terminate for all executions that the checker must not report an error.

We can look at it together after you have updated your models.

Thanks,
Ankush

[ankushdesai]

Did this help?

[ghost]

Yes, I forgot to pull the latest version of the repo.