Search

In this paper, we study the partitioning of a context-aware shared memory data structure so that it can be implemented as a distributed data structure running on multiple machines. By context-aware data structures, we mean that the result of an operation not only depends upon the value of the shared data but also upon the previous operations performed by the same client. While there is substantial work on designing distributed data structures, designing distributed context-aware data structures has not received much attention. We focus on singly-linked lists as a case study of the context-aware data structure. We start with a shared memory context-aware lock-free singly-linked list and show how it can be transformed into a distributed lock-free context-aware singly-linked list. The main challenge in such a transformation is to preserve properties of client-visible operations of the underlying data structure. We present two protocols that preserve these properties of client-visible operations of the linked list. In the first protocol, the distribution is done in the background as a low priority task, while in the second protocol the client-visible operations help the task of distribution without affecting client latency. In both protocols, the client-visible operations remain lock-free. Also, our transformation approach does not utilize any hardware primitives (except a compare-and-swap operation on a single word). We note that our transformation is generic and can be used for other lock-free context-aware data structures that can be constructed from singly-linked lists.

Lattice-linear systems allow nodes to execute asynchronously. We introduce eventually lattice-linear algorithms, where lattices are induced only among the states in a subset of the state space. The algorithm guarantees that the system transitions to a state in one of the lattices. Then, the algorithm behaves lattice linearly while traversing to an optimal state through that lattice. We present a lattice-linear self-stabilizing algorithm for service demand based minimal dominating set (SDMDS) problem. Using this as an example, we elaborate the working of, and define, eventually lattice-linear algorithms. Then, we present eventually lattice-linear self-stabilizing algorithms for minimal vertex cover (MVC), maximal independent set (MIS), graph colouring (GC) and 2-dominating set problems (2DS). Algorithms for SDMDS, MVCc and MIS converge in 1 round plus $n$ moves (within $2n$ moves), GC in $n+4m$ moves, and 2DS in 1 round plus $2n$ moves (within $3n$ moves). These results are an improvement over the existing literature. We also present experimental results to show performance gain demonstrating the benefit of lattice-linearity., Comment: arXiv admin note: text overlap with arXiv:2109.13216

In this work, we focus on the problem of replay clocks (RepCL). The need for replay clocks arises from the observation that analyzing distributed computation for all desired properties of interest may not be feasible in an online environment. These properties can be analyzed by replaying the computation. However, to be beneficial, such replay must account for all the uncertainty that is possible in a distributed computation. Specifically, if event 'e' must occur before 'f' then the replay clock must ensure that 'e' is replayed before 'f'. On the other hand, if 'e' and 'f' could occur in any order then replay should not force an order between them. After identifying the limitations of existing clocks to provide the replay primitive, we present RepCL and identify an efficient representation for the same. We demonstrate that RepCL can be implemented with less than four integers for 64 processes for various system parameters if clocks are synchronized within 1 ms. Furthermore, the overhead of RepCL (for computing/comparing timestamps and message size) is proportional to the size of the clock. Using simulations, we identify the expected overhead of RepCL based on the given system settings. We also identify how a user can the identify feasibility region for RepCL. Specifically, given the desired overhead of RepCL, it identifies the region where unabridged replay is possible.

In this paper, we study the problem of gathering distance-1 myopic robots on an infinite triangular grid. We show that the algorithm developed by Goswami et al. (SSS, 2022) is lattice-linear (cf. Gupta and Kulkarni, SRDS 2023). This implies that a distributed scheduler, assumed therein, is not required for this algorithm: it runs correctly in asynchrony. It also implies that the algorithm works correctly even if the robots are equipped with a unidirectional \textit{camera} to see the neighbouring robots (rather than an omnidirectional one, which would be required under a distributed scheduler). Due to lattice-linearity, we can predetermine the point of gathering. We also show that this algorithm converges in $2n$ rounds, which is lower than the complexity ($2.5(n+1)$ rounds) that was shown in Goswami et al.

Consider the execution of a sequential algorithm that requires the program to converge to an optimal state, and then terminate/stutter. To design such an algorithm, we need to ensure that the state space that it traverses forms a directed acyclic graph (DAG) and its sink nodes are optimal states. However, if we run the same algorithm on multiple computing nodes running in parallel, and without synchronization, it may not reach an optimal state. In most parallel processing algorithms designed in the literature, a synchronization primitive is assumed. Synchronization ensures that the nodes read fresh value, and the execution proceeds systematically, such that the subject algorithm traverses a DAG induced among the global states. With this observation, we investigate the conditions that guarantee that the execution of an algorithm is correct even if it is executed in parallel and without synchronization. To this end, we introduce DAG-inducing problems and DAG-inducing algorithms. We show that induction of a $\prec$-DAG (induced among the global states -- that forms as a result of a partial order induced among the local states visited by individual nodes) is a necessary and sufficient condition to allow an algorithm to run in asynchrony. In the paper, we first give a comprehensive description of DAG-inducing problems and DAG-inducing algorithms, along with some simple examples. Then we show some properties of an algorithm that is tolerant to asynchrony, which include the above-mentioned condition.

In this paper, we study the lattice linearity of multiplication and modulo operations. We demonstrate that these operations are lattice linear and the parallel processing algorithms that we study for both these operations are able to exploit the lattice linearity of their respective problems. This implies that these algorithms can be implemented in asynchronous environments, where the nodes are allowed to read old information from each other. These algorithms also exhibit snap-stabilizing properties, i.e., starting from an arbitrary state, the sequence of state transitions made by the system strictly follows its specification.

Consensus and leader election are fundamental problems in distributed systems. Consensus is the problem in which all processes in a distributed computation must agree on some value. Average consensus is a popular form of consensus, where the agreed upon value is the average of the initial values of all the processes. In a typical solution for consensus, each process learns the value of others' to determine the final decision. However, this is undesirable if processes want to keep their values secret from others. With this motivation, we present a solution to privacy-preserving average consensus, where no process can learn the initial value of any other process. Additionally, we augment our approach to provide outlier resistance, where extreme values are not included in the average calculation. Privacy is fully preserved at every stage, including preventing any process from learning the identities of processes that hold outlier values. To our knowledge, this is the first privacy-preserving average consensus algorithm featuring outlier resistance. In the context of leader election, each process votes for the one that it wants to be the leader. The goal is to ensure that the leader is elected in such a way that each vote remains secret and the sum of votes remain secret during the election. Only the final vote tally is available to all processes. This ensures that processes that vote early are not able to influence the votes of other processes. We augment our approach with shallow ranked voting by allowing processes to not only vote for a single process, but to designate a secondary process to vote towards in the event that their primary vote's candidate does not win the election., Comment: 10 pages + references, 2 figures, 2 algorithms, 7 theorems

Lattice-linearity was introduced as modelling problems using predicates that induce a lattice among the global states (Garg, SPAA 2020). Such modelling enables permitting asynchronous execution in multiprocessor systems. A key property of \textit{the predicate} representing such problems is that it induces \textit{one} lattice in the state space. Such representation guarantees the execution to be correct even if nodes execute asynchronously. However, many interesting problems do not exhibit lattice-linearity. This issue was alleviated with the introduction of eventually lattice-linear algorithms (Gupta and Kulkarni, SSS 2021). They induce \textit{single or multiple} lattices in a subset of the state space even when the problem cannot be defined by a predicate under which the states form a lattice. In this paper, we focus on analyzing and differentiating between lattice-linear problems and algorithms. We introduce a new class of algorithms called \textit{fully lattice-linear algorithms}. These algorithms partition the \textit{entire} reachable state space into \textit{one or more lattices}. For illustration, we present lattice-linear self-stabilizing algorithms for minimal dominating set (MDS) and graph colouring (GC) problems, and a parallel processing lattice-linear 2-approximation algorithm for vertex cover (VC). The algorithms for MDS and GC converge in {\boldmath $n$} moves and {\boldmath $n+2m$} moves respectively. These algorithms preserve this time complexity while allowing the nodes to execute asynchronously, where these nodes may execute based on old or inconsistent information about their neighbours. The algorithm for VC is the first lattice-linear approximation algorithm for an NP-Hard problem; it converges in {\boldmath $n$} moves., Comment: arXiv admin note: text overlap with arXiv:2209.14703

This paper focuses on analyzing and differentiating between lattice linear problems and algorithms. It introduces a new class of algorithms called \textit{(fully) lattice linear algorithms}. A property of these algorithms is that they induce a partial order among all states and form \textit{multiple lattices}. An initial state locks in one of these lattices. We present a lattice linear self-stabilizing algorithm for minimal dominating set.

In this report, we consider the impact of the consistency model on checkpointing and rollback algorithms for distributed shared memory. In particular, we consider specific implementations of four consistency models for distributed shared memory, namely, linearizability, sequential consistency, causal consistency and eventual consistency, and develop checkpointing and rollback algorithms that can be integrated into the implementations of the consistency models. Our results empirically demonstrate that the mechanisms used to implement stronger consistency models lead to simpler or more efficient checkpointing algorithms.

We focus on the problem of timing errors in navigation camera as a case study in a broader problem of the effect of a timing error in cyber-physical systems. These systems rely on the requirement that certain things happen at the same time or certain things happen periodically at some period $T$. However, as these systems get more complex, timing errors can occur between the components thereby violating the assumption about events being simultaneous (or periodic). We consider the problem of a surgical navigation system where optical markers detected in the 2D pictures taken by two cameras are used to localize the markers in 3D space. A predefined array of such markers, known as a reference element, is used to navigate the corresponding CAD model of a surgical instrument on patient's images. The cameras rely on the assumption that the pictures from both cameras are taken exactly at the same time. If a timing error occurs then the instrument may have moved between the pictures. We find that, depending upon the location of the instrument, this can lead to a substantial error in the localization of the instrument. Specifically, we find that if the actual movement is $\delta$ then the observed movement may be as high as $5\delta$ in the operating range of the camera. Furthermore, we also identify potential issues that could affect the error in case there are changes to the camera system or to the operating range.

In this article, we focus on extending the notion of lattice linearity to self-stabilizing programs. Lattice linearity allows a node to execute its actions with old information about the state of other nodes and still preserve correctness. It increases the concurrency of the program execution by eliminating the need for synchronization among its nodes. The extension -- denoted as eventually lattice linear algorithms -- is performed with an example of the service-demand based minimal dominating set (SDDS) problem, which is a generalization of the dominating set problem; it converges in $2n$ moves. Subsequently, we also show that the same approach could be used in various other problems including minimal vertex cover, maximal independent set and graph coloring.

Synchronization is the Achilles heel of concurrent programs. Synchronization requirement is often used to ensure that the execution of the concurrent program can be serialized. Without synchronization requirement, a program suffers from consistency violations. Recently, it was shown that if programs are designed to tolerate such consistency violation faults (\cvf{s}) then one can obtain substantial performance gain. Previous efforts to analyze the effect of \cvf-tolerance are limited to run-time analysis of the program to determine if tolerating \cvf{s} can improve the performance. Such run-time analysis is very expensive and provides limited insight. In this work, we consider the question, `Can static analysis of the program predict the benefit of \cvf-tolerance?' We find that the answer to this question is affirmative. Specifically, we use static analysis to evaluate the cost of a \cvf and demonstrate that it can be used to predict the benefit of \cvf-tolerance. We also find that when faced with a large state space, partial analysis of the state space (via sampling) also provides the required information to predict the benefit of \cvf-tolerance. Furthermore, we observe that the \cvf-cost distribution is exponential in nature, i.e., the probability that a \cvf has a cost of $c$ is $A.B^{-c}$, where $A$ and $B$ are constants, i.e., most \cvf{s} cause no/low perturbation whereas a small number of \cvf{s} cause a large perturbation. This opens up new aveneus to evaluate the benefit of \cvf-tolerance.

Physical clocks provide more precision than applications can use. For example, a 64 bit NTP clock allows a precision of 233 picoseconds. In this paper, we focus on whether the least significant bits that are not useful to the applications could be used to track (one way) causality among events. We present PWC (Physical clock With Causality) that uses the extraneous bits in the physical clock. We show that PWC is very robust to errors in clock skew and transient errors. We show that PWC can be used as both a physical and logical clock for a typical distributed application even if just 6-9 extraneous bits (corresponding to precision of 15-120 nanoseconds) are available. Another important characteristic of PWC is that the standard integer < operation can be used to compare timestamps to deduce (one-way) causality among events. Thus, PWC is significantly more versatile than previous approaches for using the physical clock to provide causality information., Comment: 11 pages, preprint version of submission to ICDCN with Appendix

In this paper, we evaluate and compare the performance of two approaches, namely self-stabilization and rollback, to handling consistency violating faults (\cvf) that occur when a self-stabilizing distributed graph-based program is executed on an eventually consistent key-value store. Consistency violating faults are caused by reading wrong values due to weaker level of consistency provided by the key-value store. One way to deal with these faults is to utilize rollback whereas another way is to rely on the property of self-stabilization that is expected to provide recovery from arbitrary states. We evaluate both these approaches in different case studies --planar graph coloring, arbitrary graph coloring, and maximal matching-- as well as for different problem dimensions such as input data characteristics, workload partition, and network latency. We also consider the effect of executing non-stabilizing algorithm with rollback with a similar stabilizing algorithm that does not utilize rollback., Comment: arXiv admin note: text overlap with arXiv:1910.08248

Monitoring distributed systems to ensure their correctness is a challenging and expensive but essential problem. It is challenging because while execution of a distributed system creates a partial order among events, the monitor will typically observe only one serialization of that partial order. This means that even if the observed serialization is consistent with the system specifications, the monitor cannot assume that the system is correct because some other unobserved serialization can be inconsistent with the system specifications. Existing solutions that guarantee identification of all such unobserved violations require some combination of lots of time and large clocks, e.g. O(n) sized Vector Clocks. We present a new, efficient two-layered monitoring approach that overcomes both the time and space limitations of earlier monitors. The first layer is imprecise but efficient and the second layer is precise but (relatively) inefficient. We show that the combination of these two layers reduces the cost of monitoring by 85-95%. Furthermore, the two-layered monitor permits the use of O(1) sized Hybrid Logical Clocks.

In this paper, we evaluate and compare the performance of two approaches, namely self-stabilization and rollback, to handling consistency violation faults (cvf) that occurred when a distributed program is executed on eventually consistent key-value store. We observe that self-stabilization is usually better than rollbacks in our experiments. Moreover, when we aggressively allow more cvf in exchange of eliminating mechanisms for guaranteeing atomicity requirements of actions, we observe the programs in our case studies achieve a speedup between 2--15 times compared with the standard implementation. We also analyze different factors that contribute to the results. Our results and analysis are useful in helping a system designer choose proper design options for their program.

Consistency properties provided by most key-value stores can be classified into sequential consistency and eventual consistency. The former is easier to program with but suffers from lower performance whereas the latter suffers from potential anomalies while providing higher performance. We focus on the problem of what a designer should do if he/she has an algorithm that works correctly with sequential consistency but is faced with an underlying key-value store that provides a weaker consistency. We propose a detect-rollback based approach: The designer identifies a correctness predicate, say $P$, and continues to run the protocol, as our system monitors $P$. If $P$ is violated (because of weaker consistency), the system rolls back and resumes the computation at a state where $P$ holds. We evaluate this approach with graph-based applications running on the Voldemort key-value store. Our experiments with deployment on Amazon AWS EC2 instances shows that using eventual consistency with monitoring can provide a $50\%$ -- $80\%$ increase in throughput when compared with sequential consistency. We also observe that the overhead of the monitoring itself was low (typically less than $4\%$) and the latency of detecting violations was small. In particular, in a scenario designed to intentionally cause a large number of violations, more than $99.9\%$ of violations were detected in less than 50 milliseconds in regional networks, and in less than 3 seconds in global networks. We find that for some applications, frequent rollback can cause the program using eventual consistency to effectively \textit{stall}. We propose alternate mechanisms for dealing with re-occurring rollbacks. Overall, for applications considered in this paper, we find that even with rollback, eventual consistency provides better performance than using sequential consistency., Comment: arXiv admin note: substantial text overlap with arXiv:1805.11453, arXiv:1801.07319

In the modern era of multi-core systems, the main aim is to utilize the cores properly. This utilization can be done by concurrent programming. But developing a flawless and well-organized concurrent program is difficult. Software Transactional Memory Systems (STMs) are a convenient programming interface which assist the programmer to access the shared memory concurrently without worrying about consistency issues such as priority-inversion, deadlock, livelock, etc. Another important feature that STMs facilitate is compositionality of concurrent programs with great ease. It composes different concurrent operations in a single atomic unit by encapsulating them in a transaction. Many STMs available in the literature execute read/write primitive operations on memory buffers. We represent them as Read-Write STMs or RWSTMs. Whereas, there exist some STMs (transactional boosting and its variants) which work on higher level operations such as insert, delete, lookup, etc. on a hash-table. We refer these STMs as Object Based STMs or OSTMs. The literature of databases and RWSTMs say that maintaining multiple versions ensures greater concurrency. This motivates us to maintain multiple version at higher level with object semantics and achieves greater concurrency. So, this paper pro-poses the notion of Optimized Multi-version Object Based STMs or OPT-MVOSTMs which encapsulates the idea of multiple versions in OSTMs to harness the greater concurrency efficiently., Comment: 45 pages

To utilize the multi-core processors properly concurrent programming is needed. Concurrency control is the main challenge while designing a correct and efficient concurrent program. Software Transactional Memory Systems (STMs) provides ease of multithreading to the programmer without worrying about concurrency issues such as deadlock, livelock, priority inversion, etc. Most of the STMs works on read-write operations known as RWSTMs. Some STMs work at high-level operations and ensure greater concurrency than RWSTMs. Such STMs are known as Object-Based STMs (OSTMs). The transactions of OSTMs can return commit or abort. Aborted OSTMs transactions retry. But in the current setting of OSTMs, transactions may starve. So, we proposed a Starvation-Free OSTM (SF-OSTM) which ensures starvation-freedom in object based STM systems while satisfying the correctness criteria as co-opacity. Databases, RWSTMs and OSTMs say that maintaining multiple versions corresponding to each key of transaction reduces the number of aborts and improves the throughput. So, to achieve greater concurrency, we proposed Starvation-Free Multi-Version OSTM (SF-MVOSTM) which ensures starvation-freedom while storing multiple versions corresponding to each key and satisfies the correctness criteria such as local opacity. To show the performance benefits, We implemented three variants of SF-MVOSTM (SF-MVOSTM, SF-MVOSTM-GC and SF-KOSTM) and compared it with state-of-the-art STMs., Comment: 68 pages, 24 figures. arXiv admin note: text overlap with arXiv:1709.01033

Causal consistency is an intermediate consistency model that can be achieved together with high availability and performance requirements even in presence of network partitions. In the context of partitioned data stores, it has been shown that implicit dependency tracking using timestamps is more efficient than explicit dependency tracking. Existing time-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 time-based algorithm, CausalSpartanX, 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 CausalSpartanX decreases the visibility latency for a given data item compared with existing time-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. CausalSpartanX also provides causally consistent distributed read-only transactions. CausalSpartanX read-only transactions are non-blocking and require only one round of communication between the client and the servers. Also, the slowdowns of partitions that are unrelated to a transaction do not affect the performance of the transaction. Like previous protocols, CausalSpartanX 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.

Eventual consistency is a popular consistency model for geo-replicated data stores. Although eventual consistency provides high performance and availability, it can cause anomalies that make programming complex for application developers. Session guarantees can remove some of these anomalies while causing much lower overhead compared with stronger consistency models. In this paper, we provide a protocol for providing session guarantees for NuKV, a key-value store developed for services with very high availability and performance requirements at eBay. NuKV relies on the Raft protocol for replication inside datacenters, and uses eventual consistency for replication among datacenters. We provide modified versions of conventional session guarantees to avoid the problem of slowdown cascades in systems with large numbers of partitions. We also use Hybrid Logical Clocks to eliminate the need for delaying write operations to satisfy session guarantees. Our experiments show that our protocol provides session guarantees with a negligible overhead when compared with eventual consistency.

In this paper, we focus on the implementation of distributed programs in using a key-value store where the state of the nodes is stored in a replicated and partitioned data store to improve performance and reliability. Applications of such algorithms occur in weather monitoring, social media, etc. We argue that these applications should be designed to be stabilizing so that they recover from an arbitrary state to a legitimate state. Specifically, if we use a stabilizing algorithm then we can work with more efficient implementations that provide eventual consistency rather than sequential consistency where the data store behaves as if there is just one copy of the data. We find that, although the use of eventual consistency results in consistency violation faults (cvf) where some node executes its action incorrectly because it relies on an older version of the data, the overall performance of the resulting protocol is better. We use experimental analysis to evaluate the expected improvement. We also identify other variations of stabilization that can provide additional guarantees in the presence of eventual consistency.Finally, we note that if the underlying algorithm is not stabilizing, even a single \cvf may cause the algorithm to fail completely thereby making it impossible to benefit from this approach., Comment: submission to ICDCN 2018

Limitations of the CAP theorem imply that if availability is desired in the presence of network partitions, one must sacrifice sequential consistency, a consistency model that is more natural for system design. We focus on the problem of what a designer should do if he/she has an algorithm that works correctly with sequential consistency but is faced with an underlying key-value store that provides a weaker (e.g., eventual or causal) consistency. We propose a detect-rollback based approach: The designer identifies a correctness predicate, say $P$, and continues to run the protocol, as our system monitors $P$. If $P$ is violated (because the underlying key-value store provides a weaker consistency), the system rolls back and resumes the computation at a state where $P$ holds. We evaluate this approach with practical graph applications running on the Voldemort key-value store. Our experiments with deployment on Amazon AWS EC2 instances shows that using eventual consistency with monitoring can provide a $50-80\%$ increase in throughput when compared with sequential consistency. We also show that the overhead of the monitoring itself is low (typically less than 4\%) and the latency of detecting violations is small. In particular, more than $99.9\%$ of violations are detected in less than $50$ milliseconds in regional AWS networks, and in less than $5$ seconds in global AWS networks., Comment: arXiv admin note: substantial text overlap with arXiv:1801.07319

Causal consistency for key-value stores has two main requirements (1) do not make a version visible if some of its dependencies are invisible as it may violate causal consistency in the future and (2) make a version visible as soon as possible so that clients have the most recent information (to the extent feasible). These two requirements conflict with each other. Existing key-value stores that provide causal consistency (or detection of causal violation) utilize a static approach in the trade-off between these requirements. Depending upon the choice, it assists some applications and penalizes some applications. We propose an alternative where the system provides a set of tracking groups and checking groups. This allows the application to choose the settings that are most suitable for that application. Furthermore, these groups can be dynamically changed based on application requirements.

Limitations of CAP theorem imply that if availability is desired in the presence of network partitions, one must sacrifice sequential consistency, a consistency model that is more natural for system design. We focus on the problem of what a designer should do if she has an algorithm that works correctly with sequential consistency but is faced with an underlying key-value store that provides a weaker (e.g., eventual or causal) consistency. We propose a detect-rollback based approach: The designer identifies a correctness predicate, say P , and continue to run the protocol, as our system monitors P . If P is violated (because the underlying key-value store provides a weaker consistency), the system rolls back and resumes the computation at a state where P holds. We evaluate this approach in the Voldemort key-value store. Our experiments with deployment of Voldemort on Amazon AWS shows that using eventual consistency with monitoring can provide 20 - 40% increase in throughput when compared with sequential consistency. We also show that the overhead of the monitor itself is small (typically less than 8%) and the latency of detecting violations is very low. For example, more than 99.9% violations are detected in less than 1 second., Comment: This paper is submitted to ICDCS 2018

We present our framework DKVF that enables one to quickly prototype and evaluate new protocols for key-value stores and compare them with existing protocols based on selected benchmarks. Due to limitations of CAP theorem, new protocols must be developed that achieve the desired trade-off between consistency and availability for the given application at hand. Hence, both academic and industrial communities focus on developing new protocols that identify a different (and hopefully better in one or more aspect) point on this trade-off curve. While these protocols are often based on a simple intuition, evaluating them to ensure that they indeed provide increased availability, consistency, or performance is a tedious task. Our framework, DKVF, enables one to quickly prototype a new protocol as well as identify how it performs compared to existing protocols for pre-specified benchmarks. Our framework relies on YCSB (Yahoo! Cloud Servicing Benchmark) for benchmarking. We demonstrate DKVF by implementing four existing protocols --eventual consistency, COPS, GentleRain and CausalSpartan-- with it. We compare the performance of these protocols against different loading conditions. We find that the performance is similar to our implementation of these protocols from scratch. And, the comparison of these protocols is consistent with what has been reported in the literature. Moreover, implementation of these protocols was much more natural as we only needed to translate the pseudocode into Java (and add the necessary error handling). Hence, it was possible to achieve this in just 1-2 days per protocol. Finally, our framework is extensible. It is possible to replace individual components in the framework (e.g., the storage component).

In the modern era of multicore processors, utilizing cores is a tedious job. Synchronization and communication among processors involve high cost. Software transaction memory systems (STMs) addresses this issues and provide better concurrency in which programmer need not have to worry about consistency issues. Another advantage of STMs is that they facilitate compositionality of concurrent programs with great ease. Different concurrent operations that need to be composed to form a single atomic unit is achieved by encapsulating them in a single transaction. In this paper, we introduce a new STM system as multi-version object based STM (MVOSTM) which is the combination of both of these ideas for harnessing greater concurrency in STMs. As the name suggests MVOSTM, works on a higher level and maintains multiple versions corresponding to each key. We have developed MVOSTM with the unlimited number of versions corresponding to each key. In addition to that, we have developed garbage collection for MVOSTM (MVOSTM-GC) to delete unwanted versions corresponding to the keys to reduce traversal overhead. MVOSTM provides greater concurrency while reducing the number of aborts and it ensures compositionality by making the transactions atomic. Here, we have used MVOSTM for the list and hash-table data structure as list-MVOSTM and HT- MVOSTM. Experimental results of list-MVOSTM outperform almost two to twenty fold speedup than existing state-of-the-art list based STMs (Trans-list, Boosting-list, NOrec-list, list-MVTO, and list-OSTM). HT-MVOSTM shows a significant performance gain of almost two to nineteen times better than existing state-of-the-art hash-table based STMs (ESTM, RWSTMs, HT-MVTO, and HT-OSTM). MVOSTM with list and hash-table shows the least number of aborts among all the existing STM algorithms. MVOSTM satisfies correctness-criteria as opacity., Comment: 35 pages, 23 figures

Networks protocols are the heart of communication networks. An efficient network protocol does maximum utilization of the underlying network capabilities. Network Protocol synthesis is the process of synthesizing or deriving network specific protocols from the requirements of a given specific network. In this report, we present a step-by-step approach for the automated synthesis of network protocols from the network specifications. Using SMT solvers to automate the protocol generation is the key idea behind the presented synthesis approach. The protocols generated using this approach followed the most optimal way of data transmission for the given network requirements.

Software Transactional Memory systems (STMs) have garnered significant interest as an elegant alternative for addressing synchronization and concurrency issues with multi-threaded programming in multi-core systems. Client programs use STMs by issuing transactions. STM ensures that transaction either commits or aborts. A transaction aborted due to conflicts is typically re-issued with the expectation that it will complete successfully in a subsequent incarnation. However, many existing STMs fail to provide starvation freedom, i.e., in these systems, it is possible that concurrency conflicts may prevent an incarnated transaction from committing. To overcome this limitation, we systematically derive a novel starvation free algorithm for multi-version STM. Our algorithm can be used either with the case where the number of versions is unbounded and garbage collection is used or where only the latest K versions are maintained, KSFTM. We have demonstrated that our proposed algorithm performs better than existing state-of-the-art STMs., Comment: 53 Pages, 11 figures

In this paper, we discuss the feasibility of monitoring partially synchronous distributed systems to detect latent bugs, i.e., errors caused by concurrency and race conditions among concurrent processes. We present a monitoring framework where we model both system constraints and latent bugs as Satisfiability Modulo Theories (SMT) formulas, and we detect the presence of latent bugs using an SMT solver. We demonstrate the feasibility of our framework using both synthetic applications where latent bugs occur at any time with random probability and an application involving exclusive access to a shared resource with a subtle timing bug. We illustrate how the time required for verification is affected by parameters such as communication frequency, latency, and clock skew. Our results show that our framework can be used for real-life applications, and because our framework uses SMT solvers, the range of appropriate applications will increase as these solvers become more efficient over time., Comment: Technical Report corresponding to the paper accepted at Runtime Verification (RV) 2017

Stabilization is a key dependability property for dealing with unanticipated transient faults, as it guarantees that even in the presence of such faults, the system will recover to states where it satisfies its specification. One of the desirable attributes of stabilization is the use of bounded space for each variable. In this paper, we present an algorithm that transforms a stabilizing program that uses variables with unbounded domain into a stabilizing program that uses bounded variables and (practically bounded) physical time. While non-stabilizing programs (that do not handle transient faults) can deal with unbounded variables by assigning large enough but bounded space, stabilizing programs that need to deal with arbitrary transient faults cannot do the same since a transient fault may corrupt the variable to its maximum value. We show that our transformation algorithm is applicable to several problems including logical clocks, vector clocks, mutual exclusion, leader election, diffusing computations, Paxos based consensus, and so on. Moreover, our approach can also be used to bound counters used in an earlier work by Katz and Perry for adding stabilization to a non-stabilizing program. By combining our algorithm with that earlier work by Katz and Perry, it would be possible to provide stabilization for a rich class of problems, by assigning large enough but bounded space for variables., Comment: Moved some content from the Appendix to the main paper, added some details to the transformation algorithm and to its description

Causal consistency is in an intermediate consistency model that can be achieved together with high availability and high performance requirements even in presence of network partitions. There are several proposals in the literature for causally consistent data stores. Thanks to the use of single scalar physical clocks, GentleRain has a throughput higher than other proposals such as COPS or Orbe. However, both of its correctness and performance relay on monotonic synchronized physical clocks. Specifically, if physical clocks go backward its correctness is violated. In addition, GentleRain is sensitive on the clock synchronization, and clock skew may slow write operations in GenlteRain. In this paper, we want to solve this issue in GenlteRain by using Hybrid Logical Clock (HLC) instead of physical clocks. Using HLC, GentleRain protocl is not sensitive on the clock skew anymore. In addition, even if clocks go backward, the correctness of the system is not violated. Furthermore, by HLC, we timestamp versions with a clock very close to the physical clocks. Thus, we can take causally consistency snapshot of the system at any give physical time. We call GentleRain protocol with HLCs GentleRain+. We have implemented GentleRain+ protocol, and have evaluated it experimentally. GentleRain+ provides faster write operations compare to GentleRain that rely solely on physical clocks to achieve causal consistency. We have also shown that using HLC instead of physical clock does not have any overhead. Thus, it makes GentleRain more robust on clock anomalies at no cost.