[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Modelling "eventually, with probability 1"
- From: Igor Konnov <igor.konnov@xxxxxxxxx>
- Date: Wed, 5 May 2021 09:45:46 +0200
- Cc: Igor Konnov <igor.konnov@xxxxxxxxx>
- Ironport-hdrordr: A9a23:TcuNIa9M8SHsbpXiLlBuk+AAI+orLtY04lQ7vn1ZYxpTb8CeioSSh/wdzxD5k3I8X3snlNCGNsC7IE/035hz/IUXIPOeTBDr0VHHEKhO5ZbvqgeNJwTQ7ehYvJ0LT4FbKPndSWd3ltz75g7QKb0d6eKK+qypmuvSpk0FJT1CUb1q7AtyF2+gfXFeeQ8uP/cEKKY=
- References: <CAFteovKBZYaJtoRsYKPG7rsQOVqNxu3d=p5n4bfigxvSqS0o=Q@mail.gmail.com>
I agree, your reasoning looks circular to me. Basically, the theorem states that <>done should hold by assuming <>done in Live.
However, it’s a nice idea to reduce a probabilistic argument to a non-probabilistic one. We did something similar for the Ben-Or’s algorithm in the paper that is not related to TLA+. However, the reduction argument required a hand-written proof to reason about adversaries and limits, see Section 7 in . I am not sure about how much of it could be mechanized.
> On 04.05.2021, at 23:28, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:
> I'm trying to model a consensus algorithm, in which a common coin (a distributed random number) is used to overcome the FLP impossibility.
> An example of such an algorithm is presented in https://eprint.iacr.org/2016/199.pdf, Figure 11.
> The termination of the algorithm is based on the fact that by repeating the coin flips we will get the needed value eventually (because of the uniform randomness, as I understand).
> The below spec does not model the entire algorithm, just the part with the common coin.
> Does it look reasonable to model that "eventual" with <>done as a fairness assumption?
> I'm not sure. It sounds a bit like assuming the conclusion, but on the other hand I'm not trying to prove that probabilistic property, just use it.
> In this example Decides looks similar to Live, but in the final spec the Decides property would be different.
> ------------- MODULE CommonCoinConverges --------------
> EXTENDS TLAPS
> VARIABLE val
> VARIABLE done
> vars == <<val, done>>
> Round == /\ ~done
> /\ \E newCoin \in BOOLEAN : \* Take a new random number.
> /\ done' = (newCoin = val) \* Check, if the value is lucky.
> /\ val' = newCoin
> Terminated == done /\ UNCHANGED vars \* Just to avoid a deadlock in a proof bellow.
> Init == /\ val \in BOOLEAN
> /\ done = FALSE
> Next == Round \/ Terminated
> Live == <>done
> Spec == Init /\ [Next]_vars /\ Live
> TypeOK == /\ val \in BOOLEAN
> /\ done \in BOOLEAN
> Decides == <>done
> THEOREM Spec => TypeOK /\ Decides
> As a side note, I managed to prove the above theorem in TLAPS from the updated_enabled_cdot branch by looking
> at https://github.com/tlaplus/tlapm/blob/updated_enabled_cdot/examples-draft/SimpleExampleWF.tla.
> Although I'm still not sure if I would be able to do that again :) The proof tactics for temporal operators are not clear to me.
> Maybe there is a paper or a book on such tactics that I should read before trying to prove something like this? :)
> THEOREM Spec => TypeOK /\ Decides
> <1>1. Spec => TypeOK
> <2>1. Init => TypeOK BY DEF Init, TypeOK
> <2>2. TypeOK /\ [Next]_vars => TypeOK'
> <3> SUFFICES ASSUME TypeOK, Next PROVE TypeOK' BY DEF vars, TypeOK
> <3> CASE Round BY DEF Round, TypeOK
> <3> CASE Terminated BY DEF Terminated, TypeOK, vars
> <3>q. QED BY DEF TypeOK, Next, Round, Terminated
> <2>q. QED BY <2>1, <2>2, PTL DEF Spec
> <1>2. Spec => Decides
> <2>x. TypeOK /\ Spec =>  (~done \/ done)
> <3>1. ASSUME TypeOK /\ [Next]_vars PROVE ~done \/ done'
> <4> SUFFICES ASSUME TypeOK, Next PROVE ~done \/ (done') BY <3>1 DEF vars
> <4> CASE Round BY DEF Round
> <4> CASE Terminated BY DEF Terminated, vars
> <4> QED BY DEF Next
> <3>q. QED BY <3>1, <1>1, PTL DEF Spec
> <2>q. QED BY <1>1, <2>x, PTL DEF Spec, Live, Decides
> <1>q. QED BY <1>1, <1>2
> Karolis Petrauskas
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovKBZYaJtoRsYKPG7rsQOVqNxu3d%3Dp5n4bfigxvSqS0o%3DQ%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E25C481E-0232-4281-AF35-4D0DE8748165%40gmail.com.