arXiv subjects

Andrea Cerone

Publications and source records attributed to Andrea Cerone.

5 recordsLinked to original sources

arXiv2019

Data Consistency in Transactional Storage Systems: a Centralised Approach

We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and partial client views. We provide operational definitions of consistency models for our key-value stores which are shown to be equivalent to the well-known declarative definitions of consistency model for execution graphs. We explore two immediate applications of our semantics: specific protocols of geo-replicated databases (e.g. COPS) and partitioned databases (e.g. Clock-SI) can be shown to be correct for a specific consistency model by embedding them in our centralised semantics; programs can be directly shown to have invariant properties such as robustness results against a weak consistency model.

cs.LO↗

arXiv2017

Algebraic Laws for Weak Consistency (Extended Version)

Modern distributed systems often rely on so called weakly-consistent databases, which achieve scalability by sacrificing the consistency guarantee of distributed transaction processing. Such databases have been formalised in two different styles, one based on abstract executions and the other based on dependency graphs. The choice between these styles has been made according to intended applications: the former has been used to specify and verify the implementation of these databases, and the latter to prove properties of programs running on top of the databases. In this paper, we present a set of novel algebraic laws (i.e. inequations) that connect these two styles of specifications; the laws relate binary relations used in a specification based on abstract executions, to those used in a specification based on dependency graphs. We then show that this algebraic connection gives rise to so called robustness criteria, conditions which ensures that a program running on top of a weakly-consistent database does not exhibit anomalous behaviours due to this weak consistency. These criteria make it easy to reason about programs running on top of these databases, and may become a basis for dynamic or static program analyses. For a certain class of consistency models specifications, we prove a full abstraction result that connects the two styles of specifications.

cs.LO↗

arXiv2015

Modelling MAC-Layer Communications in Wireless Systems

We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of such wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this LTS provide a sound proof method for proving systems contextually equivalence. We illustrate the usefulness of the proof methodology by a series of examples. Finally we show that this proof method is also complete, for a large class of systems.

cs.LO↗

arXiv2013

Modelling Probabilistic Wireless Networks

We propose a process calculus to model high level wireless systems, where the topology of a network is described by a digraph. The calculus enjoys features which are proper of wireless networks, namely broadcast communication and probabilistic behaviour. We first focus on the problem of composing wireless networks, then we present a compositional theory based on a probabilistic generalisation of the well known may-testing and must-testing pre- orders. Also, we define an extensional semantics for our calculus, which will be used to define both simulation and deadlock simulation preorders for wireless networks. We prove that our simulation preorder is sound with respect to the may-testing preorder; similarly, the deadlock simulation pre- order is sound with respect to the must-testing preorder, for a large class of networks. We also provide a counterexample showing that completeness of the simulation preorder, with respect to the may testing one, does not hold. We conclude the paper with an application of our theory to probabilistic routing protocols.

cs.LO↗

arXiv2010

Process Behaviour: Formulae vs. Tests (Extended Abstract)

Process behaviour is often defined either in terms of the tests they satisfy, or in terms of the logical properties they enjoy. Here we compare these two approaches, using extensional testing in the style of DeNicola, Hennessy, and a recursive version of the property logic HML. We first characterise subsets of this property logic which can be captured by tests. Then we show that those subsets of the property logic capture precisely the power of tests.

cs.LO↗