Counting Constraints in Flat Array Fragments: some case studies


Valid XHTML 1.0 Strict
Valid CSS!

  Abstract

Enriching logic formalisms with counting capabilities is an important task in view of the needs of many application areas, ranging from database theory to formal verification. Such enrichments have been designed both in the description logics area and in the area of Satisfiability Modulo Theories (SMT), where some of the most important recent achievements were decidability and complexity bounds for BAPA - the enrichment of Presburger arithmetic with the ability of talking about finite sets and their cardinalities. BAPA constraints can be used for program analysis and verification by expressing data structure invariants, simulations between program fragments or termination conditions. The analysis of BAPA constraints was successfully extended also to formalisms encompassing multisets as well as direct/inverse images along relations and functions.

A limitation of BAPA and its extensions lies in the fact that only uninterpreted symbols (for sets, relations, functions, etc.) are allowed. On the other hand, it is well-known that a different logical formalism, namely unary counting quantifiers, can be used in order to reason about the cardinality of definable (i.e. of interpreted) sets. Unary counting quantifiers can be added to Presburger arithmetic without compromising decidability; however they might be quite problematic if combined in an unlimited way with free function symbols. In this work, we investigate the extension of Presburger arithmetic including both counting quantifiers and uninterpreted function symbols, and we isolate fragments where we can achieve decidability and in some cases also relatively good complexity bounds. The key ingredient to isolate such fragments is the notion of flatness: roughly, in a flat formula, subterms of the kind a(t) (where a is a free function symbol) can occur only if t is a variable. By itself, this naif flatness requirement is useless (any formula can match it to the price of introducing extra quantified variables); in order to make it effective, further syntactic restrictions should be incorporated in it. This is what we are going to do in this work, where suitable notions of `flat' and `simple flat' formulae are introduced in the rich context of Presburger arithmetic enriched with free function symbols and with unary counting quantifiers (we use free function symbols to model arrays).

The fragments we design are all obviously more expressive than BAPA, but they do not come from pure logic motivations, on the contrary they are suggested by an emerging application area, namely the area of verification of fault-tolerant distributed systems. Such systems are modeled as partially synchronous systems, where a finite number of identical processes operate in lock-step (in each round they send messages, receive messages, and update their local state depending on the local state at the beginning of the round and the received messages). Messages can be lost, processes may omit to perform some tasks or also behave in a malicious way; for these reasons, the fact that some actions are enabled or not, and the correctness of the algorithms themselves, are subject to threshold conditions saying for instance that some qualified majority of processes are in a certain status or behave in a non-faulty way. Verifications tasks thus have to handle cardinality constraints of the kind studied in this work.

The framework and the results underlying our implementation are described in the paper [1] by Francesco Alberti and Silvio Ghilardi and Elena Pagani, Counting Constraints in Flat Array Fragments, available here as a preliminary research report.

  Index

We implemented a prototype ArCa-Sat producing out of simple E-flat formulae the proof obbligations (written in SMT-LIB2 format), exploiting the heuristics we devised. To experiment the feasibility of our approach for concrete verification problems, we also implemented a (beta) version of a tool called ArCa producing out of the specification of a parametric distributed system and of a safety-like problem, some E-flat simple formulae whose unsatisfiability formalizes invariant-checking (IC), bounded-model checking (BMC), and safety (SAF) problems. A script executing in sequence ArCa, ArCa-Sat and z3 can then solve such problems by reporting a `sat/unsat' answer.

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

We formalized the following algorithms:

  Code

In this section, the models developed with the counter specification are supplied, in ArCa language. In the following, we distinguish between unlimited safety properties (SAF) proved through invariants, and limited safety properties (SAF_n) tested via a BMC problem up to a a given number n of rounds. We have included, besides invariants needed to establish safety properties, also some additional `hand-crafted' ones (loosely related to the non-safety properties). All models include either the BMC / SAF_n problem, the IC / SAF problem or both. In some cases (namely: BBP Relay property, OT Irrevocability property, SRBP Relay property) we (i) split the property test into two parts (i.e., a preliminary safety property and the BMC problem), and (ii) model a `liveness-like' problem for the previously mentioned safety problem showing that - if the initial conditions of the safety problem are violated - then an execution exists such that a sat outcome is achieved.
In order to replicate our experiments, the scripts in Tools section must be used, with the provided command line.

Algorithm Property Problem ArCa model
BBP Correctness with N > 3f BMC + IC [Download]
BBP Unforgeability with N > 3f SAF_n + SAF [Download]
BBP Unforgeability with N >= 3f SAF_n [Download]
BBP Relay with N > 3f -- preliminary safety SAF_n + SAF [Download]
BBP Relay with N > 3f BMC [Download]
BBP Relay with N > 3f -- Liveness-like problem BMC (sat) [Download]
OT Agreement with threshold > 2N/3 BMC + IC [Download]
OT Agreement with threshold <= 2N/3 BMC [Download]
OT Irrevocability with threshold > 2N/3 -- preliminary safety SAF_n + SAF [Download]
OT Irrevocability with threshold > 2N/3 SAF_n + SAF [Download]
OT Irrevocability with threshold > 2N/3 -- Liveness-like problem BMC (sat) [Download]
OT Irrevocability with threshold <= 2N/3 SAF_n [Download]
OT Weak Validity with threshold > 2N/3 BMC + IC [Download]
OT Weak Validity with threshold <= 2N/3 BMC [Download]
SRBP Correctness with >= (f+1) inits BMC + IC [Download]
SRBP Correctness with <= f inits BMC [Download]
SRBP Unforgeability with >= (f+1) inits SAF_n + SAF [Download]
SRBP Relay with >= (f+1) inits -- preliminary safety SAF_n + SAF [Download]
SRBP Relay with >= (f+1) inits BMC + IC [Download]
SRBP Relay with >= (f+1) inits -- Liveness-like problem BMC (sat) [Download]
UV Integrity BMC + IC [Download]
UV Agreement with P_nosplit violated BMC [Download]
UV Irrevocability with P_nosplit violated SAF_n [Download]
U_{T,E;α} Integrity with α=0 and P_safe violated BMC [Download]
U_{T,E;α} Integrity with α=0 and P_safe BMC [Download]
U_{T,E;α} Integrity with α=1 and P_safe violated BMC [Download]
U_{T,E;α} Integrity with α=1 and P_safe BMC [Download]
U_{T,E;α} Agreement with α=0 and P_safe violated BMC [Download]
U_{T,E;α} Agreement with α=0 and P_safe BMC [Download]
U_{T,E;α} Agreement with α=1 and P_safe violated BMC [Download]
U_{T,E;α} Agreement with α=1 and P_safe BMC [Download]
MESI Cache coherence IC [Download]
MOESI Cache coherence IC [Download]

  Tools

We have developed translators that take as input our models, and produce in output a z3 file. From this page, interested readers may download our software. Specifically, for Linux systems the needed software is:

Building instructions (Linux 32/64 bits)

All the supplied scripts assume that all the models, the software of ArCa, ArCa-Sat and arca.py, and the scripts *.sh themselves, stay in the same directory; z3 must be installed and executable from command line (i.e., the PATH environment variable must be appropriately set to this purpose).

Warning: the shell scripts remove all previously created traces before running. The whole.sh and wholeInvar.sh scripts also remove the current content of the LOG subdirectory. The onemodel.sh and oneInvariant.sh scripts remove the previously produced log file for the model under verification.

ArCa-Sat: Instructions for executing arcasat as a stand-alone solver can be found here; an example of a problem specification is available here.

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.

  Results

Algorithm Property Problem Result Time (seconds)* Max Depth
*Timings have been obtained on an Intel Core i7 running Linux Ubuntu 14.04 64 bits.
BBP Correctness with N > 3f BMC SAFE 6.17 10
BBP Correctness with N > 3f IC SAFE 0.46 -
BBP Unforgeability with N > 3f SAF_n SAFE 0.25 10
BBP Unforgeability with N > 3f SAF SAFE 0.46 -
BBP Unforgeability with N >= 3f SAF_n UNSAFE 0.25 10
BBP Relay with N > 3f (preliminary safety) SAF_n SAFE 0.37 10
BBP Relay with N > 3f (preliminary safety) SAF SAFE 0.36 -
BBP Relay with N > 3f BMC SAFE 1.01 10
BBP Relay with N > 3f (Liveness-like problem) BMC sat 0.51 10
OT Agreement with threshold > 2N/3 BMC SAFE 278.95 10
OT Agreement with threshold > 2N/3 IC SAFE 14.27 -
OT Agreement with threshold <= 2N/3 BMC UNSAFE 17.75 10
OT Irrevocability with threshold > 2N/3 (preliminary safety) SAF_n SAFE 8.72 10
OT Irrevocability with threshold > 2N/3 (preliminary safety) SAF SAFE 1.39 -
OT Irrevocability with threshold > 2N/3 /td> SAF_n SAFE 0.32 10
OT Irrevocability with threshold > 2N/3 /td> SAF SAFE 1.32 -
OT Irrevocability with threshold > 2N/3 (Liveness-like problem) BMC sat 8.84 10
OT Irrevocability with threshold <= 2N/3 SAF_n UNSAFE 9.51 10
OT Weak Validity with threshold > 2N/3 BMC SAFE 0.45 10
OT Weak Validity with threshold <= 2N/3 IC SAFE 2.25 -
OT Weak Validity with threshold <= 2N/3 BMC UNSAFE 0.59 10
SRBP Correctness with >= (f+1) inits BMC SAFE 0.82 10
SRBP Correctness with >= (f+1) inits IC SAFE 0.32 -
SRBP Correctness with <= f inits BMC UNSAFE 2.21 10
SRBP Unforgeability with >= (f+1) inits SAF_n SAFE 0.85 10
SRBP Unforgeability with >= (f+1) inits SAF SAFE 1.46 -
SRBP Relay with >= (f+1) inits (preliminary safety) SAF_n SAFE 0.66 10
SRBP Relay with >= (f+1) inits (preliminary safety) SAF SAFE 1.42 -
SRBP Relay with >= (f+1) inits BMC SAFE 1.93 10
SRBP Relay with >= (f+1) inits IC SAFE 0.31 -
SRBP Relay with >= (f+1) inits (Liveness-like problem) BMC sat 1.19 10
UV Integrity BMC SAFE 1.02 10
UV Integrity IC SAFE 22.79 -
UV Agreement with P_nosplit violated BMC UNSAFE 4.18 10
UV Irrevocability with P_nosplit violated SAF_n UNSAFE 2.04 10
U_{T,E;α} Integrity with α=0 and P_safe violated BMC UNSAFE 0.83 10
U_{T,E;α} Integrity with α=0 and P_safe BMC SAFE 1.16 10
U_{T,E;α} Integrity with α=1 and P_safe violated BMC UNSAFE 4.93 10
U_{T,E;α} Integrity with α=1 and P_safe BMC SAFE 5.20 10
U_{T,E;α} Agreement with α=0 and P_safe violated BMC UNSAFE 7.78 10
U_{T,E;α} Agreement with α=0 and P_safe BMC SAFE 59.80 10
U_{T,E;α} Agreement with α=1 and P_safe violated BMC UNSAFE 31.94 10
U_{T,E;α} Agreement with α=1 and P_safe BMC SAFE 179.67 10
MESI Cache coherence IC SAFE 0.11 -
MOESI Cache coherence IC SAFE 0.08 -

  Bibliography

[1]F. Alberti, S. Ghilardi, E. Pagani,
Counting Constraints in Flat Array Fragments.
In Proc. IJCAR, 2016.
[2]M. Biely, B. Charron-Bost, A. Gaillard, M. Hutle, A. Schiper, and J. Widder.
Tolerating corrupted communication.
In Proc. PODC, pages 244-253, 2007.
[3]N. Björner, K.v. Gleissenthall, and A. Rybalchenko.
Synthesizing cardinality invariants for parameterized systems.
2015. Manuscript.
[4]B. Charron-Bost and A. Schiper.
The heard-of model: computing in distributed systems with benign faults.
Distributed Computing, pages 49-71, 2009.
[5]M.S. Papamarcos and J.H. Patel.
A low-overhead coherence solution for multiprocessors with private cache memories.
In Proc. ISCA, page 348, 1984.
[6]Y. Solihin.
Fundamentals of Parallel Computer Architecture Multichip and Multi-core Systems.
Solihin Publishing & Consulting LLC, 2008.
[7]T.K. Srikanth and S. Toueg.
Optimal clock synchronization.
Journal of the ACM, 34(3):626-645, 1987.
[8]T.K. Srikanth and S. Toueg.
Simulating authenticated broadcasts to derive simple fault-tolerant algorithms.
Distributed Computing, 2(2):80-94, 1987.

  Authors