Overview

The CEC Tool (or Correct Eventual Consistency Tool) is a tool, based on the CISE theory TODO: ADD LINK designed to help programmers develop distributed applications using the Hybrid Consistency model. The tool takes as input a specification of an application, written in Boogie, and outputs the coordination that should be applied to its operations, expressed through a token model.

Introduction

An integral part of developing a distributed application is choosing the consistency model that should be applied to it.

Employing strong consistency means ensuring the invariant of the application at all times but also dealing with a worse performance due to excessive coordination. On the other hand, employing eventual consistency means the inability to ensure the invariant of the application but that also comes with less performance costs.

The hybrid consistency models are a mixture of these two approaches, where coordination is only applied when it is strictly needed to maintain the application's invariant. This means having the benefit that comes with using strong consistency while cutting the performance costs associated with excessive coordination.

The CEC Tool is designed to help the development of applications that intent on using the hybrid consistency model. By analyzing a specification of the application, the tool infers what coordination that should be applied to the parameters and operations of the application. This way the application programmer is no longer tasked with choosing the coordination manually, an extremely hard and error prone task.

Installation

In order to use the tool, you must first install Boogie. You can find more information about Boogie and the installation process at https://boogie.codeplex.com/.

After you have finished installing Boogie you only have to download either the .jar or source code in order to use the CEC Tool, no additional installation process is required. Both the source code and CEC Tool's latest release can be found in the Git Hub repository.

Usage

In order to run the CEC Tool you have to execute either the source code or the .jar file with the following parameters:

boogie_path library_path specification_path [-c]

• boogie_path is the command needed to execute Boogie in your system. For instance, if you're using mono to execute Boogie it should be "mono boogie". If mono and boogie aren't on the $PATH variable, it should be "<path to mono>/mono <path to boogie>/boogie".

• library_path is the path to the directory that contains the libraries you're importing in your specification. More about libraries can be found here.

• specification_path is the path to the application specification for which coordination will be generated. Here you can find more about out to create one of these specifications.

• -c is an optional parameter. Using it means the tool will execute the specification correction tests besides executing the concurrency related ones.

Application Specifications and Libraries

In here you can find, explained in a step by step manner, how to create an application specification from scratch.

Additionally, here it is explained in detail how to create and use libraries.

Analysis and Output

The tool performs a systematic analysis on the application specification given as input. This analysis first checks the correction of said specification (note that this first step is optional) and afterwards runs several verifications in order to infer which is the coordination that should be applied to the application.

The tool is able to infer which coordination should be applied both at the operation level and, in some cases, at the parameter level too.

The output coordination inferred by the tool is expressed through a token model.

You can find a more detailed explanation of the analysis process and of the output of the tool here.