Hello again, Evgeniy,
Hello Stephan,
Thanks so much for your clarification! After excluding heardof from state view I got exactly those results stated in the table.
> Anyway, we only included these experiments in order to demonstrate the interest of the theorem shown earlier in the paper
Yeah.
As far as I understand, the main idea of the paper is that an algorithm expressed in HO model can be model-checked with respect to
'local property' in coarse-grained model without loosing any meaningful states compared to fine-grained model.
Exactly (but the theorem is independent of the verification technology and applies just as well to model checking as to deductive verification, where it leads to simpler proofs). Not sure if this forum is a right place for such a side note but anyway:
As far as I understand HO model by some reasons is especially well-suited for consensus algorithms, but as for some mutual exclusion algorithms it is not so.
Indeed, the Heard-Of computational model is intended for representing fault-tolerant distributed algorithms, it will not be appropriate for mutual exclusion algorithms. I was wondering if HO model can be extended with N, number of alive processes as seen by environment fault detector on the current round, as a parameter giving
more expressive power to the model.
I don't understand this: first, HO has no notion of fault detector, but of course the Heard-Of set HO(p,r) can be seen as the complement of the set D(p,r) of faulty processes signaled to process p in round r in the RRFD model by Gafni. Thus, the number of processes that p considers alive in round r is precisely the cardinality of HO(p,r), so "extending" the model by this information would not add any information?
It may resemble RRFD by Gafni, but actually it still abstracts concrete set of suspected/alive processes into just a number.
Potentially this could lead to a bigger class of algorithms checkable/provable in a reasonable time with a help of (extended) reduction theorem.
It is then takes its place somewhere in the middle between rather concrete RRFD and rather abstract HO.
Maybe you have investigated something similar towards this line of thought?
No, I haven't. We restricted attention to the HO model of algorithms.
Regards, Stephan вторник, 18 апреля 2017 г., 19:59:11 UTC+3 пользователь Stephan Merz написал: Hi Evgeniy,
thanks for your interest in this paper. The modules that I used are attached to this message, and I think they are equivalent to what you have, modulo comments, renaming, and some auxiliary definitions. The difference in performance comes from the fact that I used a VIEW specification so that TLC identifies any two states that only differ in the value of the auxiliary (history) variable heardof, as indicated in the last sentence of section 4 of the paper (p.13): this variable is useful essentially for interpreting counter-examples displayed by TLC but does not affect the behavior of the algorithm. In particular, it is not referred to by any predicate that is used in the specification. I am sorry if the explanation/hint in the paper is a little cryptic.
Anyway, we only included these experiments in order to demonstrate the interest of the theorem shown earlier in the paper: they are extremely naive as far as model checking fault-tolerant algorithms goes. If you really want to learn about model checking this kind of algorithm, I suggest that you look at the recent work by Igor Konnov et al. [1].
Best regards,
Stephan
-- 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+u...@xxxxxxxxxxxxxxxx.To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.Visit this group at https://groups.google.com/group/tlaplus.For more options, visit https://groups.google.com/d/optout.
|