Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems

We develop quantifier elimination procedures for a fragment of higher order logic arising from the formalization of distributed systems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of Pre/Post images and of projections.

We show in particular that our procedures are quite effective in producing counter abstractions that can be model-checked using standard SMT technology. In fact, quite often in the current literature verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by our specifically designed technique for second order quantifier elimination.

We implemented our procedure in a simplified (but still expressive) subfragment and we showed that our method is able to successfully handle verification benchmarks from various sources with interesting performances.

The framework and the results underlying our implementation are described in the paper [1] by Silvio Ghilardi and Elena Pagani, Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems, currently submitted to a Journal.
Interested readers may find preliminary workshop versions in [11][12].

We designed a restricted input specification language for our tool ArcaSim. ArcaSim accepts system specifications matching the syntactic format explained in the original paper, and produces as output a file in the Horn SMT_Lib format, ready to be model-checked e.g. by μZ [14], the fixpoint engine of the SMT solver Z3. In successful cases, μZ produces an invariant (entirely expressed in terms of our counters) which guarantees the safety of the original system.

In the next sections (Code section and Results section) there are respectively the files used with ArcaSim and some experimental statistics. In the Tools section, the tools used to translate the models into models for Z3 are available.

We analyzed several benchmarks representative of different classes of problems. We list below the considered classes, and the algorithms studied for each class:

• agreement algorithms with either benign or malicious failures
• the One-Third algorithm (OT) [5] for consensus in the presence of benign transmission failures
• the Byzantine Broadcast Primitive (BBP) [22] used to simulate agreement in the presence of byzantine failures
• the Uniform Voting (UV) algorithm [7] for consensus in the presence of benign transmission failures
• the Coordinated Uniform Voting (CoUV) algorithm [7] for consensus in the presence of benign transmission failures
• the Simplified Coordinated Uniform Voting (SiCoUV) algorithm [7] for consensus in the presence of benign transmission failures
• the U_T,E,α algorithm [4] for consensus in the presence of byzantine failures
• the Send-Receive Broadcast Primitive (SRBP) [21] to synchronize clocks in systems with benign failures
• Ben-Or's Consensus algorithm [3] for asynchronous systems with byzantine failures
• agreement and reliable multicast algorithms with crash failures
• the FloodSet [17] algorithm for Consensus
• the FloodMin [17] algorithm for the k-agreement problem
• the FC [19] algorithm for Consensus
• the EDAC [8] algorithm for Consensus
• the UTRB1 [2] algorithm for Uniform Timed Reliable Broadcast problem
• cache coherence and mutual exclusion algorithms
• the MESI [18] and MOESI [20] algorithms for cache coherence.
• the Dekker's algorithm [9] for mutual exclusion.

Furthermore, some benchmarks are used for qualitative comparison with the ByMC tool proposed in the literature [16]:

• STRB [22] is the same as BBP although modeled so as to mimic the ByMC model
• ABA [6] solves the asynchronous byzantine agreement problem
• NBAC [13] solves the non-blocking atomic commitment problem
• FRB [10] solves the reliable broadcast problem in asynchronous systems with crash failures

In this section, the models developed with the counter specification are supplied, in ArcaSim language. In some cases (namely: BBP Relay property, SRBP Relay property, UTRB1 Integrity property) we split the property test into two parts.
A zip archive is also available containing all developed models.

In order to replicate our experiments, the scripts in Tools section must be used, with the provided command line.

Algorithm	Property	Conditions	ArcaSim model
OT	Agreement	t ≥ 2N/3	[Download]
OT	Agreement	t < 2N/3	[Download]
OT	Weak Validity	t ≥ 2N/3	[Download]
OT	Weak Validity	t < 2N/3	[Download]
OT	Irrevocability	t ≥ 2N/3	[Download]
OT	Irrevocability	t < 2N/3	[Download]
BBP	Correctness	t < N/3	[Download]
BBP	Correctness	t ≤ N/3	[Download]
BBP	Unforgeability	t < N/3	[Download]
BBP	Unforgeability	t ≤ N/3	[Download]
BBP	Relay (I)	t < N/3	[Download]
BBP	Relay (I)	t ≤ N/3	[Download]
BBP	Relay (II)	t < N/3	[Download]
BBP	Relay (II)	t ≤ N/3	[Download]
UV	Integrity	--	[Download]
UV	Agreement	no Pnosplit	[Download]
UV	Irrevocability	no Pnosplit	[Download]
CoUV	Integrity	--	[Download]
CoUV	Agreement	no Pnosplit	[Download]
CoUV	Irrevocability	no Pnosplit	[Download]
SiCoUV	Integrity	--	[Download]
SiCoUV	Agreement	no Pnosplit	[Download]
SiCoUV	Irrevocability	no Pnosplit	[Download]
UT,E,α	Integrity	α =0 ∧ no Psafe	[Download]
UT,E,α	Integrity	α =0 ∧ Psafe	[Download]
UT,E,α	Integrity	α =1 ∧ no Psafe	[Download]
UT,E,α	Integrity	1 ≤ α < N/2 ∧ no Psafe	[Download]
UT,E,α	Integrity	α =1 ∧ Psafe	[Download]
UT,E,α	Integrity	1 ≤ α < N/2 ∧ Psafe	[Download]
UT,E,α	Agreement	α =0 ∧ no Psafe	[Download]
UT,E,α	Agreement	α =0 ∧ Psafe	[Download]
UT,E,α	Agreement	α =1 ∧ no Psafe	[Download]
UT,E,α	Agreement	1 ≤ α < N/2 ∧ no Psafe	[Download]
UT,E,α	Agreement	α =1 ∧ Psafe	[Download]
UT,E,α	Agreement	1 ≤ α < N/2 ∧ Psafe	[Download]
SRBP	Correctness	t < N/2 ∧ ≥ (f+1) inits	[Download]
SRBP	Correctness	t < N/2 ∧ ≥ f inits	[Download]
SRBP	Unforgeability	t < N/2 ∧ ≥ (f+1) inits	[Download]
SRBP	Relay (I)	t < N/2 ∧ no echo	[Download]
SRBP	Relay (II)	t < N/2 ∧ 1 echo	[Download]
Ben-Or	Validity	t < N/5	[Download]
Ben-Or	Validity	t ≤ N/3	[Download]
Ben-Or	Agreement	t < N/5	[Download]
Ben-Or	Agreement	t ≤ N/3	[Download]

Algorithm	Property	Conditions	ArcaSim model
FloodSet	Weak Validity	--	[Download]
FloodSet	Agreement	--	[Download]
FloodMin	Weak Validity	k=1 ∧ |V|=2	[Download]
FloodMin	Strong Validity	k=1 ∧ |V|=2	[Download]
FloodMin	k-agreement	k=1 ∧ |V|=2	[Download]
FloodMin	Weak Validity	k=1 ∧ |V|=3	[Download]
FloodMin	Strong Validity	k=1 ∧ |V|=3	[Download]
FloodMin	k-agreement	k=1 ∧ |V|=3	[Download]
FloodMin	Weak Validity	k=2 ∧ |V|=3	[Download]
FloodMin	Strong Validity	k=2 ∧ |V|=3	[Download]
FloodMin	k-agreement	k=2 ∧ |V|=3	[Download]
FC	Strong Validity	|V|=2	[Download]
FC	Agreement	|V|=2	[Download]
EDAC	Weak Validity	|V|=2	[Download]
EDAC	Agreement	|V|=2	[Download]
UTRB1	Validity	--	[Download]
UTRB1	Uniform Agreement	--	[Download]
UTRB1	Integrity (I)	--	[Download]
UTRB1	Integrity (II)	--	[Download]

Algorithm	Property	Conditions	ArcaSim model
MESI	Cache coherence	--	[Download]
MOESI	Cache coherence	--	[Download]
Dekker	Mutual exclusion	--	[Download]

Algorithm	Property	Conditions	ArcaSim model
STRB	Correctness	N > 3t	[Download]
STRB	Unforgeability	N > 3t	[Download]
ABA	Correctness	N > 3t	[Download]
ABA	Unforgeability	N > 3t	[Download]
NBAC	Agreement	N > f	[Download]
NBAC	Abort-validity	N > f	[Download]
NBAC	Commit-validity	N > f	[Download]
FRB	Unforgeability	N > f	[Download]
FRB	Correctness	N > f	[Download]

We have developed both an ArcaSim implementation, and scripts that take as input our models and produce in output the verification result. From this page, interested readers may download our software; the reference page for the ArCA tools is here. Specifically, for Linux systems the needed software is:

• ArcaSim: takes as input an algorithm model in ArcaSim format, and produces a Z3 file named CounterSimulation.smt2. [64 bits architectures]
• Z3 theorem prover
• oneModel.sh: shell script that allows to translate an ArcaSim model into a Z3 file and to execute the Z3 file. It takes as input the name of a model (e.g., one of the models supplied in the Code section) without the .sim suffix. For example: "./oneModel.sh safeOT_Agree". It should be run in an examples/JAR subdirectory of ArcaSim where the source codes are placed. It assumes the existence of a LOG subdirectory, where a *.log file is created reporting the outcomes of the algorithm check. [script]
• whole.sh: shell script that allows to perform the same steps as oneModel.sh for all the models available in this page (Code section). It has no input argument. It assumes the existence of a LOG subdirectory, where an everything.log file is created, reporting the outcomes of the algorithm check for each model. [script]

Building instructions (Linux 64 bits)

Z3 must be installed and executable from command line (i.e., the PATH environment variable must be appropriately set to this purpose).

Warning: the whole.sh script removes the current content of the LOG subdirectory. The oneModel.sh script removes the previously produced log file for the model under verification.

ArcaSim: Instructions for writing a problem specification are available in the file examples/How_to_write_a_specification.

No warranty disclaim: this software is free and, as such, it comes with no warranty. By using this software, you are accepting the terms stated here. Because the program is licensed free of charge, there is no warranty for the program, to the extent permitted by applicable law. The entire risk as to the quality and performance of the program is with you. Should the program prove defective, you assume the cost of all necessary servicing, repair or correction directly or indirectly derived from its use.

This section reports, for each one of the considered models, the number of transitions produced by the ArcaSim tool and its running time, the running time of Z3 to check the CounterSimulation.smt2 file produced by ArcaSim and its outcome.

Algorithm	Property	Conditions	ArcaSim		Z3
			# trans.	Time (s.) *	Time (s) *	Answer
*Timings have been obtained on an Intel Core i7i7-7700 processor 3.60 GHz and operating system Linux Ubuntu 18.04 (64 bits).
OT	Agreement	t ≥ 2N/3	11	0.58	0.50	sat
OT	Agreement	t < 2N/3	14	0.80	0.01	unsat
OT	Weak Validity	t ≥ 2N/3	11	0.62	0.01	sat
OT	Weak Validity	t < 2N/3	14	0.81	0.01	sat
OT	Irrevocability	t ≥ 2N/3	22	1.61	0.87	sat
OT	Irrevocability	t < 2N/3	28	2.23	0.07	unsat
BBP	Correctness	t < N/3	7	0.43	0.04	sat
BBP	Correctness	t ≤ N/3	7	0.41	0.03	sat
BBP	Unforgeability	t < N/3	7	0.40	0.03	sat
BBP	Unforgeability	t ≤ N/3	7	0.41	0.02	unsat
BBP	Relay (I)	t < N/3	7	0.42	0.01	sat
BBP	Relay (I)	t ≤ N/3	7	0.42	0.01	sat
BBP	Relay (II)	t < N/3	6	0.38	0.03	sat
BBP	Relay (II)	t ≤ N/3	6	0.39	0.03	sat
UV	Integrity	--	21	15.36	0.07	sat
UV	Agreement	no Pnosplit	21	19.85	0.03	unsat
UV	Irrevocability	no Pnosplit	36	38.62	0.16	unsat
CoUV	Integrity	--	15	288.66	0.14	sat
CoUV	Agreement	no Pnosplit	15	333.29	0.10	sat
CoUV	Irrevocability	no Pnosplit	23	408.05	0.04	unsat
SiCoUV	Integrity	--	11	257.81	0.04	sat
SiCoUV	Agreement	no Pnosplit	11	284.13	0.06	sat
SiCoUV	Irrevocability	no Pnosplit	19	410.09	1.04	sat
UT,E,α	Integrity	α =0 ∧ no Psafe	17	7.95	0.04	unsat
UT,E,α	Integrity	α =0 ∧ Psafe	30	13.14	0.10	sat
UT,E,α	Integrity	α =1 ∧ no Psafe	14	6.74	0.05	unsat
UT,E,α	Integrity	1 ≤ α < N/2 ∧ no Psafe	14	6.75	0.06	unsat
UT,E,α	Integrity	α =1 ∧ Psafe	26	11.52	0.13	sat
UT,E,α	Integrity	1 ≤ α < N/2 ∧ Psafe	26	11.52	0.21	sat
UT,E,α	Agreement	α =0 ∧ no Psafe	17	10.73	0.10	unsat
UT,E,α	Agreement	α =0 ∧ Psafe	30	17.66	0.90	sat
UT,E,α	Agreement	α =1 ∧ no Psafe	14	8.99	0.12	unsat
UT,E,α	Agreement	1 ≤ α < N/2 ∧ no Psafe	14	8.86	0.06	unsat
UT,E,α	Agreement	α =1 ∧ Psafe	26	15.25	0.56	sat
UT,E,α	Agreement	1 ≤ α < N/2 ∧ Psafe	26	15.29	0.85	sat
SRBP	Correctness	t < N/2 ∧ ≥ (f+1) inits	9	1.25	0.02	sat
SRBP	Correctness	t < N/2 ∧ ≥ f inits	9	1.25	0.01	unsat
SRBP	Unforgeability	t < N/2 ∧ ≥ (f+1) inits	9	1.25	0.02	sat
SRBP	Relay (I)	t < N/2 ∧ no echo	9	1.26	0.02	sat
SRBP	Relay (II)	t < N/2 ∧ 1 echo	9	1.61	0.02	sat
Ben-Or	Validity	t < N/5	13	0.56	0.02	sat
Ben-Or	Validity	t ≤ N/3	21	0.89	0.13	unsat
Ben-Or	Agreement	t < N/5	13	0.83	0.08	sat
Ben-Or	Agreement	t ≤ N/3	21	1.30	0.23	unsat

Algorithm	Property	Conditions	ArcaSim		Z3
			# trans.	Time (s.) *	Time (s) *	Answer
*Timings have been obtained on an Intel Core i7i7-7700 processor 3.60 GHz and operating system Linux Ubuntu 18.04 (64 bits). For some measures the time spent by Z3 was not measurable (0.00 s.) because it is below the clock tick.
FloodSet	Weak Validity	--	11	4.43	0.02	sat
FloodSet	Agreement	--	11	5.18	0.03	sat
FloodMin	Weak Validity	k=1 ∧ |V|=2	9	1.37	0.01	sat
FloodMin	Strong Validity	k=1 ∧ |V|=2	9	1.42	0.01	sat
FloodMin	k-agreement	k=1 ∧ |V|=2	9	1.59	0.03	sat
FloodMin	Weak Validity	k=1 ∧ |V|=3	17	11.84	0.05	sat
FloodMin	Strong Validity	k=1 ∧ |V|=3	17	10.30	0.02	sat
FloodMin	k-agreement	k=1 ∧ |V|=3	17	13.03	0.08	sat
FloodMin	Weak Validity	k=2 ∧ |V|=3	17	11.78	0.06	sat
FloodMin	Strong Validity	k=2 ∧ |V|=3	17	10.31	0.02	sat
FloodMin	k-agreement	k=2 ∧ |V|=3	17	13.06	0.05	sat
FC	Strong Validity	|V|=2	9	13.92	0.03	sat
FC	Agreement	|V|=2	9	15.29	0.07	sat
EDAC	Weak Validity	|V|=2	35	46.95	0.03	sat
EDAC	Agreement	|V|=2	35	49.66	0.02	sat
UTRB1	Validity	--	2	0.13	0.06	sat
UTRB1	Uniform Agreement	--	2	0.19	0.00	sat
UTRB1	Integrity (I)	--	2	0.16	0.00	sat
UTRB1	Integrity (II)	--	2	0.15	0.00	sat

Algorithm	Property	Conditions	ArcaSim		Z3
			# trans.	Time (s.) *	Time (s) *	Answer
*Timings have been obtained on an Intel Core i7i7-7700 processor 3.60 GHz and operating system Linux Ubuntu 18.04 (64 bits). For some measures the time spent by Z3 was not measurable (0.00 s.) because it is below the clock tick.
MESI	Cache coherence	--	15	0.21	0.05	sat
MOESI	Cache coherence	--	20	0.41	0.07	sat
Dekker	Mutual exclusion	--	5	0.04	0.00	sat

Algorithm	Property	Conditions	ArcaSim		Z3		ByMC
			# trans.	Time (s.) *	Time (s) *	Answer	Time (s.) **
*Timings have been obtained on an Intel Core i7i7-7700 processor 3.60 GHz and operating system Linux Ubuntu 18.04 (64 bits). **Timings have been obtained by running the original ByMC examples provided by the virtual machine version 2.4.0 downloaded from [15] on an Intel Core i7i7-7700 processor 3.60 GHz and operating system Linux Ubuntu 18.04 (64 bits).
STRB	Correctness	N > 3t	7	0.73	0.05	sat	0.23
STRB	Unforgeability	N > 3t	7	0.74	0.03	sat	0.16
ABA	Correctness	N > 3t	6	1.79	0.01	sat	15.68
ABA	Unforgeability	N > 3t	6	1.79	0.01	sat	0.95
NBAC	Agreement	N > f	5	0.14	0.01	sat	5.01
NBAC	Abort-validity	N > f	5	0.14	0.01	sat	4.81
NBAC	Commit-validity	N > f	5	0.15	0.01	sat	4.89
FRB	Unforgeability	N > f	4	0.59	0.01	sat	0.14
FRB	Correctness	N > f	4	0.73	0.01	sat	0.18

[1]	S. Ghilardi, E. Pagani, Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems. In Journal of Automated Reasoning, vol.65, pp. 425-460 (2021). DOI: https://doi.org/10.1007/s10817-020-09578-5
[2]	O. Babaoglu and S. Toueg. Non-Blocking Atomic Commitment. In Distributed Systems - 2nd Edition, pages 147-168, Sape Mullender Ed., Addison-Wesley 1993.
[3]	M. Ben-Or. Another advantage of free choice: completely asynchronous agreement protocols. In Proc. PODC, pages 27-30, 1983.
[4]	M. Biely, B. Charron-Bost, A. Gaillard, M. Hutle, A. Schiper, and J. Widder. Tolerating corrupted communication. In Proc. PODC, pages 244-253, 2007.
[5]	N. Bjørner, K.v. Gleissenthall, and A. Rybalchenko. Cardinalities and Universal Quantifiers for Verifying Parameterized Systems. In Proc. of the 37th ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2016.
[6]	G. Bracha and S. Toueg. Asynchronous consensus and broadcast protocols. J. ACM 32 (4), pages 824-840, Oct. 1985.
[7]	B. Charron-Bost and A. Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, pages 49-71, 2009.
[8]	B. Charron-Bost and A. Schiper. Uniform consensus is harder than consensus. J. Algorithms 51(1), pages 15-37, 2004.
[9]	E.W. Dijkstra. Cooperating Sequential Processes. In Programming Languages, Academic Press, 1968.
[10]	D. Fisman, O. Kupferman, and Y. Lustig. On Verifying Fault Tolerance of Distributed Protocols. In Proc. TACAS, 2008.
[11]	S. Ghilardi, and E. Pagani. Second Order Quantifier Elimination: Towards Verification Applications. In Proc. Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dec.2017. CEUR Workshop Proceedings (CEUR-WS.org, ISSN 1613-0073), Volume 2013, pp. 36-50, 2017.
[12]	S. Ghilardi, and E. Pagani. Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. In Proc. 5th International Workshop on Proof eXchange for Theorem Proving (PxTP 2017), Sep.2017. Electronic Proceedings in Theoretical Computer Science, Vol.262, pp.39-53. DOI: 10.4204/EPTCS.262.5
[13]	R. Guerraoui. On the hardness of failure-sensitive agreement problems. Information Processing Letters 79, pages 99-104, 2001.
[14]	K. Hoder, N. Bjørner, and L. deMoura.  μZ - An Efficient Engine for Fixed Points with Constraints. In CAV, pages 457-462, 2011.
[15]	I. Konnov. ByMC: Byzantine Model Checker. http://forsyte.at/software/bymc/, last visit: Jul.17, 2018.
[16]	I. V. Konnov, H. Veith, and J. Widder. What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers, pages 6-21, 2015.
[17]	N. A. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
[18]	M.S. Papamarcos and J.H. Patel. A low-overhead coherence solution for multiprocessors with private cache memories. In Proc. ISCA, page 348, 1984.
[19]	M. Raynal. Fault-tolerant Agreement in Synchronous Message-passing Systems. Morgan & Claypool - Synthesis Lectures on Distributed Computing Theory series, 2010.
[20]	Y. Solihin. Fundamentals of Parallel Computer Architecture Multichip and Multi-core Systems. Solihin Publishing & Consulting LLC, 2008.
[21]	T.K. Srikanth and S. Toueg. Optimal clock synchronization. Journal of the ACM, 34(3):626-645, 1987.
[22]	T.K. Srikanth and S. Toueg. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing, 2(2):80-94, 1987.

• Silvio Ghilardi (reference author)
• Elena Pagani