Question about the specification of reliable broadcast algorithm by Bracha & Toueg (1985) about examples

[lemmy]

Tagging the spec authors: @konnov @banhday @josef-widder

[lduranovic]

@lemmy Thanks!

[josef-widder]

Hi @lduranovic99 , could you please clarify which spec you are referring to. I guess there might be several and the encoding of faults may differ, so to answer your second question, I want to be sure we are on the same page ;-)

Regarding the first concern, this encoding originated from our previous work on parameterized model checking threshold automata, e.g. here. This method only works on symmetric systems, so we couldn't capture a special process (the broadcaster) in an efficient manner. At the same time, we wanted to verify the threshold functionalities (t+1, n-t under resilience conditions like n>3t). Thus, we have chosen to capture the effect of the broadcaster in the initial state:

• all processes have 0: e.g., the broadcaster is correct and didn't choose to send any message.
• all processes have 1: e.g, the broadcaster is correct and thus sends to everyone
• mixed inputs: the broadcaster is faulty and sense to some (those with 1)

(Of course the "all 0s" and "all 1s" also capture the scenario where the broadcaster is "faulty", but sends or does not send consistently to everyone.)

From our initial states, a process sends echo if and only if it sends echo in executions the corresponding execution with a broadcaster. To formalize the argument, I guess I would define projections of traces that abstract away the broadcaster, and show that there is trace equivalence to the traces of the spec.

[lduranovic]

Hi @josef-widder! Thanks for the response. You can find the specific file that I was looking at here.

I think your explanation for why this specification makes sense (in terms of the broadcaster) makes sense to me, although I would be curious to see what this formalization argument for matching traces obtained by the two versions of the algorithm would look like.

I'm still very interested in the behavior of the faulty hosts, and what your thoughts are on how well this model captures the behavior of Byzantine hosts.

[josef-widder]

Thanks to your initial question, I found a bug in the encoding. I proposed a fix in #81.

However, the overall encoding is OK, and indeed it captures the non-determinism on the correct receiver that is due to faulty senders. Consider this condition that guards the increment of the counter at process i of received echo messages nRcvdE[i]

Examples/specifications/aba-asyn-byz/aba_asyn_byz.tla

Line 73 in 31f687b

\/ /\ nRcvdE[i] < nSntE + (IF includeByz THEN nByz ELSE 0)

The counter can only be incremented if it smaller than the sum of

• the number of echo messages sent by correct processes
• the number of Byzantine processes

Potentially, Byzantine processes can be assumed to have sent any message, and the adversary has the control whether and when to deliver these messages. Even if this action is enabled, it may never trigger, that is, nRcvdE[i] may never exceed nSntE.
So this kind of encoding captures the effect Byzantine nodes have on correct ones, rather than the actions of Byzantine nodes.

[ahelwer]

@josef-widder @lduranovic are there any changes that need to be made to the example spec or are we good to close this issue?

[josef-widder]

I think we can close the issue as it was mostly a question on modelling. The problem that we then found was fixed in #81.

[lduranovic]

Yeah, thanks for asking! I will go ahead and close it with this comment then.