We present our framework DKVF that enables one to quickly prototype and evaluate new consistency protocols for key-value stores. DKVF is designed based on the separation of concerns in creating distributed data stores. This separation of concerns allows the designers of consistency protocols to only focus on the high-level consistency protocols which gives them the opportunity to quickly deploy a consistency protocol and evaluate its performance. Moreover, the loose coupling of the different components allows us to easily change different components (e.g. storage engine) of an implementation. We demonstrate DKVF by implementing four existing protocols --eventual consistency, COPS, GentleRain and CausalSpartan-- with it. The implementation of these protocols was very convenient with DKVF, as it only required to write a piece of code for the consistency component that is very close to the pseudocode of the original papers. Hence, it was possible to achieve this in just 1-2 days per protocol. DKVF also comes with a toolset that facilitates running clusters and performing experiments. Tutorial video: https://www.youtube.com/watch?v=MFJQzsJkwfc&list=PLErtSVEHsnBJvoQQI6iqGn61oNrUVVuST

Causal consistency is an intermediate consistency model that can be achieved together with high availability and high-performance requirements even in presence of network partitions. In the context of partitioned data stores, it has been shown that implicit dependency tracking using clocks is more efficient than explicit dependency tracking by sending dependency check messages. Existing clock-based solutions depend on monotonic psychical clocks that are closely synchronized. These requirements make current protocols vulnerable to clock anomalies. In this paper, we propose a new clock-based algorithm, CausalSpartan, that instead of physical clocks, utilizes Hybrid Logical Clocks (HLCs). We show that using HLCs, without any overhead, we make the system robust on physical clock anomalies. This improvement is more significant in the context of query amplification, where a single query results in multiple GET/PUT operations. We also show that CausalSpartan decreases the visibility latency for a given data item comparing to existing clock-based approaches. In turn, this reduces the completion time of collaborative applications where two clients accessing two different replicas edit same items of the data store. Like previous protocols, CausalSpartan assumes that a given client does not access more than one replica. We show that in presence of network partitions, this assumption (made in several other works) is essential if one were to provide causal consistency as well as immediate availability to local updates.

We focus on protocols for auditable restoration of distributed systems. The need for such protocols arises due to conflicting requirements (e.g., access to the system should be restricted but emergency access should be provided). One can design such systems with a tamper detection approach (based on the intuition of In-case-of-emergency-break-glass). However, in a distributed system, such tampering, which are denoted as auditable events, is visible only for a single node. This is unacceptable since the actions they take in these situations can be different than those in the normal mode. Moreover, eventually, the auditable event needs to be cleared so that system resumes the normal operation. With this motivation, in this paper, we present two protocols for auditable restoration, where any process can potentially identify an auditable event. The first protocol has an unbounded state space while the second protocol uses bounded state space that does not increase with the length of the computation. In both protocols, whenever a new auditable event occurs, the system must reach an auditable state where every process is aware of the auditable event. Only after the system reaches an auditable state, it can begin the operation of restoration. Although any process can observe an auditable event, we require that only authorized processes can begin the task of restoration. Moreover, these processes can begin the restoration only when the system is in an auditable state. Our protocols are self-stabilizing and can effectively handle the case where faults or auditable events occur during the restoration protocol. Moreover, they can be used to provide auditable restoration to other distributed protocols.

In this paper, we evaluate the effectiveness of model slicing to provide assurance about correctness of SystemC TLM programs. The need for such assurance is important since SystemC has become a de-facto standard for building systems with hardware/software co-design. Existing approaches that enable one to transform the given SystemC TLM program into an UPPAAL model that can be verified suffer from models that result in state space explosion. This problem becomes even more complex when verifying fault-tolerance. Model slicing has the potential to provide a solution to this problem. Therefore, we focus on developing a model slicer that extends existing work on model slicing and combines it with tools to generate UPPAAL models from SystemC TLM programs and tools to add the impact of faults to those UPPAAL models. The experimental results show that with the proposed framework, the designer is capable of verifying even very complex SystemC TLM models, which would have been impossible without the proposed approach.

We focus on the issue of realizability constraints in the context of model repair. Model repair focuses on revising a given program to satisfy new properties of interest while satisfying existing properties such as fault-tolerance. An important difficulty in using model repair is that the repaired model must be realizable in the constraints given by the underlying system. It is well-known that these realizability constraints cause an increase in the complexity of model repair (e.g., from P to NP-complete). Hence, existing approaches for adding fault-tolerance to distributed program focuses on cautious repair where in every step, the model being repaired satisfies the realizability constraints. They also utilize heuristics to reduce the complexity of repair. In this work, we focus on using lazy repair while adding fault-tolerance. Specifically, in this work, we utilize a two-step approach. The first step ignores the realizability constraints and performs model repair to add fault-tolerance. This ensures that the resulting program satisfies the desired property of interest (namely, fault-tolerance) although it may not be realizable. The second step attempts to revise this program to ensure that realizability constraints are satisfied without creating new program behaviors. This ensures that the resulting program satisfies both the properties of interest and realizability constraints. We demonstrate that this approach is more efficient than the cautious repair algorithm in the literature. We also note that inherently the lazy repair approach is also applicable in other contexts such as synchronous systems, cyber-physical systems, etc.

In this paper, we present the paradigm of collaborative stabilization that focuses on providing stabilization in the presence of an essential but potentially disruptive environment. By essential, we mean that without the environment actions, stabilization property would be impossible. At the same time, environment actions are not in the control of the program and can be disruptive to the recovery. We demonstrate the need for collaborative stabilization by providing examples where existing paradigms of stabilization are undesirable/insufficient. We compare collaborative stabilization with existing paradigms of stabilization. We identify the complexity of verifying collaborative stabilizing programs and develop theorems that focus on composition of such programs.

In this paper, we focus on revising a given program so that the average recovery time in the presence of an adversarial scheduler is bounded by a given threshold lambda. Specifically, we consider the scenario where the fault (or other unexpected action) perturbs the program to a state that is outside its set of legitimate states. Starting from this state, the program executes its actions/transitions to recover to legitimate states. However, the adversarial scheduler can force the program to reach one illegitimate state that requires a longer recovery time. To ensure that the average recovery time is less than lambda, we need to remove certain transitions/behaviors. We show that achieving this average response time while removing minimum transitions is NP-hard. In other words, there is a tradeoff between the time taken to synthesize the program and the transitions preserved to reduce the average convergence time. We present six different heuristics and evaluate this tradeoff with case studies. Finally, we note that the average convergence time considered here requires formalization of hyperproperties. Hence, this work also demonstrates feasibility of adding (certain) hyperproperties to an existing program.

We focus on a protocol for auditable restoration of distributed systems. The need for such protocol arises due to conflicting requirements (e.g., access to the system should be restricted but emergency access should be provided). One can design such systems with a tamper detection approach (based on the intuition of "break the glass door"). However, in a distributed system, such tampering, which are denoted as auditable events, is visible only for a single node. This is unacceptable since the actions they take in these situations can be different than those in the normal mode. Moreover, eventually, the auditable event needs to be cleared so that system resumes the normal operation. With this motivation, in this paper, we present a protocol for auditable restoration, where any process can potentially identify an auditable event. Whenever a new auditable event occurs, the system must reach an "auditable state" where every process is aware of the auditable event. Only after the system reaches an auditable state, it can begin the operation of restoration. Although any process can observe an auditable event, we require that only "authorized" processes can begin the task of restoration. Moreover, these processes can begin the restoration only when the system is in an auditable state. Our protocol is self-stabilizing and can effectively handle the case where faults or auditable events occur during the restoration protocol. Moreover, it can be used to provide auditable restoration to other distributed protocol.

Availability of the service delivered by cloud providers is one of the most important QoS factors of the service level agreements between providers and customers. Since current Infrastructure-as-a-Service providers use virtualization technology to manage data centers, virtual data centers (VDCs) have become a popular infrastructure for cloud computing. In order to study the service availability, a stochastic activity network (SAN) model is presented in this paper. The proposed SAN model can be appropriately used to investigate the impact of different characteristics and policies on service availability of VDCs.