Search

Causality tracking among events is a fundamental challenge in distributed environments. Much previous work on this subject has focused on designing an efficient and scalable protocol to represent logical time. Several implementations of logical clocks have been proposed, most recently the Encoded Vector Clock (EVC), a protocol to encode Vector Clocks (VC) in scalar numbers through the use of prime numbers, to improve performance and scalability. We propose and formalize the concept of Resettable Encoded Vector Clock (REVC), a new logical clock implementation, which builds on the EVC to tackle its very high growth rate issue. We show how our REVC can be applied in both shared memory systems and message passing systems to achieve a consistent logical clock. We show, through practical examples, the advantage of REVC’s growth rate with respect to EVC’s growth rate. Finally, we show a practical application of the REVC to the dynamic race detection problem in multi-threaded environments. We compare our tool to the currently existing VC-based tool $\text{DJIT}^+$ DJIT + to show how the REVC can help in achieving higher performance with respect to the Vector Clock.

The vector clock is a fundamental tool for tracking causality in distributed applications. Unfortunately, it does not scale well to large systems because each process needs to maintain a vector of size n , where n is the total number of processes in the system. To address this problem, we propose the prime clock, which is based on the encoding of the vector clock using prime numbers and uses a single number to represent vector time. We propose the operations on the encoded vector clock (EVC). We then show how to timestamp global states and how to perform operations on the global states using the EVC. Using a theoretical analysis and a simulation model, we evaluate the growth rate of the size of the EVC. The EVC is seen to grow very fast and hence it does not appear to offer a general purpose practical replacement of vector clocks. To address this drawback, we propose several scalability techniques for the EVC that can allow the use of the EVC in practical applications. We then present two case studies of detecting memory consistency errors in MPI one-sided applications and of dynamic race detection in multi-threaded environments, that use a combination of two of these scalability techniques. The results show that the EVC is not just a theoretical concept, but it is applicable to practical problems and can compete in terms of both space and time requirements with other known protocols.

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 by using partially synchronized physical time. Specifically, our algorithm relies on bounded clock drift $$\epsilon $$ among processes and message delivery that either delivers the message in time $$\delta $$ or loses it. If we let $$\epsilon $$ to be as much as 100 s and $$\delta $$ to be as much as 1 h, this property is satisfied by any practical system. 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, diffusing computations, 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 work by Katz and Perry and by assuming incorruptible partially synchronized clocks, it would be possible to provide stabilization for a rich class of problems, by assigning large enough but bounded space for variables.

Many high performance computing applications have been developed by using MPI one-sided communication. The separation between data movement and synchronization poses enormous challenges for programmers in preserving the reliability of programs. One of those challenges is the detection of memory consistency errors, which are a notorious bug, degrading the reliability and performance of programs. Even an MPI expert can easily make these mistakes. The lockopts bug, which occurred in an RMA test case of the MPICH MPI implementation, is an example for this situation. MC-Checker is the most effective debugger in solving the memory consistency errors. MC-Checker did ignore the transitive ordering of the happened-before relation to ensure the acceptable overheads in terms of time complexity. Consequently, MC-Checker is prone to error due to the source of false positives attributable to the ignorance of the transitive ordering of the happened-before relation. To address this issue, we propose a time-stamping system based on the encoded vector clock to help preserve the full happened-before relation with reasonable overhead. The system is implemented in MC-CChecker, which is an enhancement of MC-Checker. The experimental findings prove that MC-CChecker not only effectively detects memory consistency errors like MC-Checker did, but also completely eliminates the potential source of false positives, which is a major limitation of MC-Checker while still retaining acceptable overheads of execution time and memory usage. Especially, MC-CChecker is fairly scalable when processing a large number of trace files generated from running the lockopts up to 8192 processes.

Testing for causality between events in distributed executions is a fundamental problem. Vector clocks solve this problem but do not scale well. The probabilistic Bloom clock can determine causality between events with lower space, time, and message-space overhead than vector clock; however, predictions suffer from false positives. We give the protocol for the Bloom clock based on Counting Bloom filters and study its properties including the probabilities of a positive outcome and a false positive. We show the results of extensive experiments to determine how these above probabilities vary as a function of the Bloom timestamps of the two events being tested, and to determine the accuracy, precision, and false positive rate of a slice of the execution containing events in the temporal proximity of each other. Based on these experiments, we make recommendations for the setting of the Bloom clock parameters. We postulate the causality spread hypothesis from the application’s perspective to indicate whether Bloom clocks will be suitable for correct predictions with high confidence. The Bloom clock design can serve as a viable space-, time-, and message-space-efficient alternative to vector clocks if false positives can be tolerated by an application.

In many scenarios, information must be disseminated over intermittently-connected environments when network infrastructure becomes unavailable. Example scenarios include disasters in which first responders need to send updates about their critical tasks. If such updates pertain to a shared data set (e.g., pins on a map), their consistent dissemination is important. We can achieve this through causal ordering and consensus. Popular consensus algorithms, such as Paxos and Raft, are most suited for connected environments with reliable links. While some work has been done on designing consensus algorithms for intermittently-connected environments, such as the One-Third Rule (OTR) algorithm, there is need to improve their efficiency and timely completion. We propose CoNICE, a framework to ensure consistent dissemination of updates among users in intermittently-connected, infrastructure-less environments. It achieves efficiency by exploiting hierarchical namespaces for faster convergence, and lower communication overhead. CoNICE provides three levels of consistency to users' views, namely replication, causality and agreement. It uses epidemic propagation to provide adequate replication ratios, and optimizes and extends Vector Clocks to provide causality. To ensure agreement, CoNICE extends basic OTR to support long-term fragmentation and critical decision invalidation scenarios. We integrate the multilevel consistency schema of CoNICE, with a naming schema that follows a topic hierarchy-based dissemination framework, to improve functionality and performance. Performing city-scale simulation experiments, we demonstrate that CoNICE is effective in achieving its consistency goals, and is efficient and scalable in the time for convergence and utilized network resources.

A distributed system guarantees the acceptance of Byzantine fault tolerance (BFT) for information transmission. Practical BFT (pBFT) and asynchronous BFT (aBFT) are among the various available forms of BFT. Distributed systems generally share information with all participating nodes. After information is shared, the systems reshare it. Thus, ensuring BFT consumes a considerable amount of time. Herein, we propose Decision search protocols that apply the gossip protocol, denoted by DecisionBFT, for distributed networks with guaranteed BFT. Each protocol in DecisionBFT is completely asynchronous and leaderless, it has an eventual consensus but no round-robin or proof-of-work. The core concept of the proposed technology is the consensus structure, which is based on the directed acyclic graph (DAG) and gossip protocol. In the most general form, each node in the algorithm has a set of k neighbors of most preference. When receiving transactions, a node creates and connects an event block with all its neighbors. Each event block is signed by the hashes of the creating node and its k peers. The consensus structure of the event blocks utilizes a DAG, which guarantees aBFT. The proposed framework uses Lamport timestamps and concurrent common knowledge. Further, an example of a Decision search algorithm, based on the gossip protocol DecisionBFT, is presented. The proposed DecisionBFT protocol can reach a consensus when 2/3 of all participants agree to an event block without any additional communication overhead. The DecisionBFT protocol relies on a cost function to identify the k peers and generate the DAG-based consensus structure. By creating a dynamic flag table that stores connection information between blocks, the gossip protocol achieves a consensus in fewer steps than that in the case of the existing aBFT protocol.

Determining the causality between events in distributed executions is a fundamental problem. Vector clocks solve this problem but do not scale well. The probabilistic Bloom filter data structure can be used as a Bloom clock to determine causality between events with lower space overhead than vector clock; however, the Bloom filter and hence the Bloom clock naturally suffer from false positives. We give a formal protocol of the Bloom clock based on Counting Bloom filters and study its properties. We formulate the probabilities of a positive outcome, a positive being false, and a false positive for Bloom clocks as a function of the corresponding vector clocks, as well as their estimates as a function of the Bloom clocks. We also indicate how to estimate the accuracy, precision, and false positive rate of an execution slice that is identified by the Bloom timestamps of two events.

It has been shown that annotating Petri nets unfoldings with time stamps allows to build distributed testers for distributed systems. However, the construction of the annotated unfolding of a distributed system currently remains a centralized task. In this paper we extend a distributed unfolding technique in order to annotate the resulting unfolding with time stamps. This allows distributed construction of distributed testers for distributed systems.

Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software. A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially. We consider the well studied notion of conflict serializability for dynamically checking atomicity. Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution. The number of edges in such a graph can grow quadratically with the length of the trace making the analysis not scalable. In this paper, we present AeroDrome, a novel single pass linear time algorithm that uses vector clocks to detect violations of conflict serializability in an online setting. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.

Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this problem is to detect if there is a pair of conflicting memory accesses that are unordered by Lamport’s happens-before (HB) relation. HB based race detection is known to not report false positives, i.e., it is sound. However, the soundness guarantee of HB only promises that the first pair of unordered, conflicting events is a schedulable data race. That is, there can be pairs of HB-unordered conflicting data accesses that are not schedulable races because there is no reordering of the events of the execution, where the events in race can be executed immediately after each other. We introduce a new partial order, called schedulable happens-before (SHB) that exactly characterizes the pairs of schedulable data races — every pair of conflicting data accesses that are identified by SHB can be scheduled, and every HB-race that can be scheduled is identified by SHB. Thus, the SHB partial order is truly sound. We present a linear time, vector clock algorithm to detect schedulable races using SHB. Our experiments demonstrate the value of our algorithm for dynamic race detection — SHB incurs only little performance overhead and can scale to executions from real-world software applications without compromising soundness.

Hybrid vector clock(s) (HVC) provide a mechanism to combine the theory and practice of distributed systems. Improving on traditional vector clock(s) (VC), HVC utilizes synchronized physical clocks to reduce the size by focusing only on causality where the physical time associated with two events is within a given uncertainty window $\epsilon$ and letting physical clock alone determine the order of events that are outside the uncertainty window. In this paper, we develop a model for determining the bounds on the size of HVC. Our model uses four parameters, $\epsilon$ : uncertainty window, $\delta$ : message delay, $\alpha$ : communication frequency and $n$ : number of nodes in the system. We derive the size of HVC in terms of a delay differential equation, and show that the size predicted by our model is almost identical to the results obtained by simulation. We also identify closed form solutions that provide tight lower and upper bounds for useful special cases. We show that for many practical applications and deployment environments in Amazon EC2, the size of HVC remains only as a couple entries and substantially less than $n$ . Finally, although the analytical results rely on a specific communication pattern they are useful in evaluating size of HVC in different communication scenarios.

In this research, we propose the Clock Synchronization by Least Common Multiple (CSLCM) method to remove the clock offset and clock skew among the sensor nodes. The proposed CSLCM enables the nodes to reach a network synchronization time by calculating the least common multiple of their Clock Time Period (CTP). The network is organized into clusters and every node reaches the network synchronization time using its own CTP. Simulation results show that, the CSLCM algorithm is more efficient compared to the Average Time Synchronization with Pairwise messages (ATSP) in terms of accuracy, communication overhead, and computation overhead.

Time synchronization is crucial for wireless sensor networks (WSNs) since it maintains data consistency, coordination, and enables other fundamental operations. Over the last decade, a number of powerful time synchronization algorithms have been proposed for clock accuracy optimization by using signal processing techniques. However, most of these algorithms attempt to estimate the clock phase offset and skew and do not correct the node's local clock at every timing packet exchange before the clock parameters are jointly estimated, which reduces the network synchronization accuracy during the estimation of clock parameters and limits the applicability of the synchronization algorithms for some practical sensor networks where a global time scale is consistently required. Motivated by this, this paper investigates the synchronization scheme of having inactive nodes overhearing the pairwise sender-receiver time synchronization based on acknowledgement with clock correction at every synchronization. Assuming exponential random delays, the maximum likelihood estimators (MLEs) of clock skew and the corresponding approximate Cramer-Rao lower bounds (CRLBs) for active and overhearing nodes are derived. In addition, we also consider a linear synchronization model that the clock skew is directly estimated. Simulation results verify the efficiency of the clock skew estimators.

Time synchronization plays an important role in the spacecraft formation flight and constellation autonomous navigation, etc. For the application of clock synchronization in a network system, it is not always true that all the observed nodes in the network are interconnected, therefore, it is difficult to achieve the high-precision time synchronization of a network system in the condition that a certain node can only obtain the measurement information of clock from a single neighboring node, but cannot obtain it from other nodes. Aiming at this problem, a novel method of high-precision time synchronization in a network system is proposed. In this paper, each clock is regarded as a node in the network system, and based on the definition of different topological structures of a distributed system, the three control algorithms of time synchronization under the following three cases are designed: without a master clock (reference clock), with a master clock (reference clock), and with a fixed communication delay in the network system. And the validity of the designed clock synchronization protocol is proved by both stability analysis and numerical simulation.

Timestamp free clock synchronization in a master–slave network, i.e., synchronization where no timestamps are exchanged between the nodes, is considered. For highly accurate synchronization, a novel discrete-valued clock model is introduced. It is based on the observation that clocks are discrete counters in digital wireless radios. Considering this model, it is shown that the round-trip time (RTT) measurements follow specific pulse or step shaped functions. The estimated parameters of these RTT functions are used to determine the clock parameters (clock skew and phase) and the propagation delay. Numerical analysis illustrate that when RTT measurements are collected using discrete-valued clocks, the proposed estimation schemes outperform estimators derived from the continuous clock model, which is used in the state-of-the-art methods. Moreover, the presented scheme performs similar to recently presented discrete-valued clock approaches with more stringent hardware assumption. The correctness of the proposed models is validated through hardware experiments.

The work solves a new problem of optimizing the boundary of buffered clock trees, which has not been addressed in the design automation as yet. Precisely, we want to show that the clock cells that directly drive flip-flops should not necessarily be buffers. By taking into account the internal structure of flip-flops, we can have a freedom of choosing either buffers or inverters for the cell implementation from library. This in fact leads to cancel out the two inverters, one in the driving buffer and another in each flip-flop, thereby reducing the power consumption on the clock tree, including flip-flops. We generalize this idea to look into the possibility of co-optimizing the driving buffers and flip-flops together to reduce the clock power at the boundary of clock trees, and propose an effective four-step synthesis algorithm of clock tree boundary for low power. By applying our proposed technique to benchmark circuits, it is observed that the clock power is able to be reduced by 4.45 % ~ 6.33 % further on average without timing violation.

Quasi-synchronous checkpointing algorithms are classified into: SZPF, ZPF and ZCF.We propose a validation approach to detect the previously mentioned properties.We model an algorithm execution into the HBR graph and IDR graph.We designed two sets of validation rules to work over the HBR graph and IDR graph.A lower cost is achieved using the IDR graph which is the minimal causal graph. The autonomic computing paradigm is oriented towards enabling complex distributed systems to manage themselves, even in faulty situations. The diagnosability analysis is a priori a study through which a system can be self-aware about its current state. It is from the determination of a consistent state that a system can take some action to repair or reconfigure itself. Nevertheless, in a distributed system it is hard to determine consistent states since we cannot observe simultaneously all the local variables of different processes. In this context, the challenge is to efficiently monitor the system execution over time to capture trace information in order to determine if the system accomplishes both functional and non-functional requirements. Quasi-synchronous checkpointing is a technique that collects information from which a system can establish consistent snapshots. Based on this technique, several checkpointing algorithms have been developed. According to the checkpoint properties detected and ensured, they are classified into: Strictly Z-Path Free (SZPF), Z-Path Free (ZPF) and Z-Cycle Free (ZCF). Generally, the method adopted for the performance evaluation of checkpointing algorithms involves simulation. However, few works have been designed to validate their correctness. In this paper, we propose an efficient validation approach based on a graph transformation oriented towards the automatic detection of the previously mentioned properties. To achieve this, we took the vector clocks resulting from an algorithm execution, and we modeled them into the happened-before graph and the immediate dependency graph (which is the minimal causal graph). Then, we designed a set of transformation rules to verify if in these graphs, the algorithm is exempt from non-desirable patterns, such as Z-paths or Z-cycles, according to the case.

We consider the problem of data race prediction where the program's behavior is represented by a trace. A trace is a sequence of program events recorded during the execution of the program. We employ the schedulable happens-before relation to characterize all pairs of events that are in a race for the schedule as manifested in the trace. Compared to the classic happens-before relation, the schedulable happens-before relations properly takes care of write-read dependencies and thus avoids false positives. The challenge is to efficiently identify all (schedulable) data race pairs. We present a refined linear time vector clock algorithm to predict many of the schedulable data race pairs. We introduce a quadratic time post-processing algorithm to predict all remaining data race pairs. This improves the state of the art in the area and our experiments show that our approach scales to real-world examples. Thus, the user can systematically examine and fix all program locations that are in a race for a particular schedule.

Deterministic replay presents challenges and often results in high memory and runtime overheads. Previous studies deterministically reproduce program outputs often only after several replay iterations or may produce a non-deterministic sequence of output to external sources. In this paper, we propose AggrePlay, a deterministic replay technique which is based on recording read-write interleavings leveraging thread-local determinism and summarized read values. During the record phase, AggrePlay records a read count vector clock for each thread on each memory location. Each thread checks the logged vector clock against the current read count in the replay phase before a write event. We present an experiment and analyze the results using the Splash2x benchmark suite as well as two real-world applications. The experimental results show that on average, AggrePlay experiences a better reduction in compressed log size, and 56% better runtime slowdown during the record phase, as well as a 41.58% higher probability in the replay phase than existing work.

In systems with non-volatile main memories (NVMMs), programmers must carefully control the order in which writes become persistent. Otherwise, what will remain in persistence after a crash may be unusable upon recovery. Prior art has already explored semantic models for specifying this persist order, but most enforcement algorithms for the order are not scalable to large server machines because they assume that the machine contains only one or two memory controllers. In this paper, we describe a collection of provably correct algorithms for enforcing the persist-order across writes, generated at many different cores, and persisted across numerous different memory controllers. Relative to existing solutions, our algorithms improve performance by 48% by reducing both traffic and serialization overheads.

Tracking causality (or happened-before relation) between events is useful for many applications such as debugging and recovery from failures. Consider a concurrent system with n threads and m objects. For such systems, either a vector clock of size n is used with one component per thread or a vector clock of size m is used with one component per object. A natural question is whether one can use a vector clock of size strictly less than the minimum of m and n to timestamp events. We give an algorithm in this paper that uses a hybrid of thread and object components. Our algorithm is guaranteed to return the minimum number of components necessary for vector clocks. We first consider the case when the interaction between objects and threads is statically known. This interaction is modeled by a thread-object bipartite graph. Our algorithm is based on finding the maximum bipartite matching of such a graph and then applying Konig-Egervary Theorem to compute the minimum vertex cover to determine the optimal number of components necessary for the vector clock. We also propose two mechanisms to compute such an vector clock when computation is revealed in an online fashion. Evaluation on different types of graphs indicates that our offline algorithm generates a size vector clock which is significantly less than the minimum of m and n. These mechanisms are more effective when the underlying bipartite graph is not dense.

Vector clock algorithms are basic wait-free building blocks that facilitate causal ordering of events. As wait-free algorithms, they are guaranteed to complete their operations within a finite number of steps. Stabilizing algorithms allow the system to recover after the occurrence of transient faults, such as soft errors and arbitrary violations of the assumptions according to which the system was designed to behave.

Task parallel programs that are free of data race are guaranteed to be deterministic, serializable, and free of deadlock. Techniques for verification of data race freedom vary in both accuracy and asymptotic complexity. One work is particularly well suited to task parallel programs with isolation and lightweight threads. It uses the Java Pathfinder model checker to reason about different schedules and proves the presence or absence of data race in a program on a fixed input. However, it uses a direct and inefficient transitive closure on the happens-before relation to reason about data race. This paper presents Zipper, an alternative to this naive algorithm, which identifies the presence or absence of data race in asymptotically superior time. Zipper is optimized for lightweight threads and, in the presence of many threads, has superior time complexity to leading vector clock algorithms. This paper includes an empirical study of Zipper and a comparison against the naive computation graph algorithm, demonstrating the superior performance it achieves.

Chapter 4 is the chapter of consistency concepts. First, the classical transactional concept of relational databases is given, including ACID (atomicity, consistency, isolation, and durability), followed by pessimistic and optimistic concurrency control mechanisms. Second, consistency issues of NoSQL databases are discussed such as the BASE (basically available, soft state, eventually consistent) concept and the CAP theorem (consistency, availability, and partition tolerance). In addition, vector clocks are introduced in order to serialize parallel transactions. A comparison between ACID and BASE closes the chapter.

The vector clock is a fundamental tool for tracking causality in parallel and distributed applications. Unfortunately, it does not scale well to large systems because each process needs to maintain a vector of size n, where n is the total number of processes in the system. To address this problem, the encoded vector clock (EVC) was recently proposed. The EVC is based on the encoding of the vector clock using prime numbers and uses a single number to represent vector time. The EVC has all the properties of the vector clock and yet uses a single number to represent global time. However, the single number EVC tends to grow fast and may soon exceed the size of the traditional vector clock. In this paper, we evaluate the growth rate of the size of the EVC using a simulation model. The simulations show that the EVC grows relatively fast, and the growth rate depends on the mix of internal events and communication events. To overcome this drawback, the EVC can be used in conjunction with several scalability techniques that can allow the use of the EVC in practical applications. We then present a case study of detecting memory consistency errors in MPI one-sided applications using EVC.

In this paper, we study the global clock synchronization problem for wireless sensor networks under unknown exponential delays in the two-way message exchange mechanism. The joint maximum likelihood estimator of clock offsets, clock skews and fixed delays for the network is formulated as a linear programming (LP) problem. Then, based on the alternating direction method of multipliers (ADMM), we propose a fully distributed synchronization algorithm which has low communication overhead and computation cost. Simulation results show that the proposed algorithm achieves better accuracy than consensus algorithm and the distributed least squares algorithm, and can always converge to the centralized optimal solution. HighlightsNetwork-wide clock synchronization problem under exponential message delays is solved.The problem is cast into a linear programming problem.ADMM is exploited to obtain a fully-distributed algorithm.Closed-from expressions are available for each update step in the algorithm.The proposed algorithm is guaranteed to converge to the global optimal solution.

We argue that grid structures are a very promising alternative to the standard approach for distributing a clock signal throughout VLSI circuits and other hardware devices. Traditionally, this is accomplished by a delay-balanced clock tree, which distributes the signal supplied by a single clock source via carefully engineered and buffered signal paths.Our approach, termed HEX, is based on a hexagonal grid with simple intermediate nodes, which both control the forwarding of clock ticks in the grid and supply them to nearby functional units. HEX is Byzantine fault-tolerant, in a way that scales with the grid size, self-stabilizing, and seamlessly integrates with multiple synchronized clock sources, as used in multi-synchronous Globally Synchronous Locally Asynchronous (GALS) architectures. Moreover, HEX guarantees a small clock skew between neighbors even for wire delays that are only moderately balanced. We provide both a theoretical analysis of the worst-case skew and simulation results that demonstrate very small typical skew in realistic runs.

Many distributed services need to be scalable: internet search, electronic commerce, e-government... In order to achieve scalability, high availability and fault tolerance, such applications rely on replicated components. Because of the dynamics of growth and volatility of customer markets, applications need to be hosted by adaptive, highly scalable systems. In particular, the scalability of the reliable multicast mechanisms used for supporting the consistency of replicas is of crucial importance. Reliable multicast might propagate updates in a pre-determined order (e.g., FIFO, total or causal). Since total order needs more communication rounds than causal order, the latter appears to be the preferable candidate for achieving multicast scalability, although the consistency guarantees based on causal order are weaker than those of total order. This paper provides a historical survey of different scalability approaches for reliable causal multicast protocols., This work was supported by European Regional Development Fund (FEDER) and Ministerio de Economia y Competitividad (MINECO) under research Grant TIN2012-37719-C03-01.

Data races are often discussed in the context of lock acquisition and release, with race-detection algorithms routinely relying on vector clocks as a means of capturing the relative ordering of events from different threads. In this paper, we present a data-race detector for a language with channel communication as its sole synchronization primitive, and provide a semantics directly tied to the happens-before relation, thus forging the notion of vector clocks.

Understanding the runtime behavior of concurrent programs is a challenging task. A popular approach is to establish a happens-before relation via vector clocks. Thus, we can identify bugs and performance bottlenecks, for example, by checking if two conflicting events may happen concurrently. We employ a two-phase method to derive vector clock information for a wide range of concurrency features that includes all of the message-passing features in Go. The first phase (instrumentation and tracing) yields a runtime trace that records all events related to message-passing concurrency that took place. The second phase (trace replay) is carried out of fline and replays the recorded traces to infer vector clock information. Trace replay operates on thread-local traces. Thus, we can observe behavior that might result from some alternative schedule. Our approach is not tied to any specific language. We have built a prototype for the Go programming language and provide empirical evidence of the usefulness of our method.

In this paper we present Nemo, a NUMA-aware Transactional Memory (TM) design and implementation optimized for promoting scalability in applications running on top of NUMA architectures. Nemo deploys a hybrid design where conflicting threads alternate the usage of single timestamps and vector clocks to identify inconsistent executions depending upon the source of conflict. We assessed the performance of Nemo by using both synthetic and well-known OLTP transactional workloads. Our approach offers improvements over the six state-of-the-art competitors we implemented.

In this paper we introduce the notion of spread net. Spread nets are (safe) Petri nets equipped with vector clocks on places and with ticking functions on transitions, and are such that vector clocks are consistent with the ticking of transitions. Such nets generalize previous families of nets like unfoldings, merged processes and trellis processes, and can thus be used to represent runs of a net in a true concurrency semantics through an operation called the spreading of a net. By contrast with previous constructions, which may identify conflicts, spread nets allow loops in time, In Proceedings ICE 2018, arXiv:1810.02053

With greater adoption of various high-level parallel programming models to harness on-node parallelism, accurate data race detection has become more crucial than ever. However, existing tools have great difficulty spotting data races through these high-level models, as they primarily target low-level concurrent execution models (e.g., concurrency expressed at the level of POSIX threads). In this paper, we propose a novel technique to accurately detect those data races that can occur at higher levels of concurrent execution. The core idea of our technique is to introduce the general concept of Thread-Local Concurrency (TLC) as a new way to translate the concurrency expressed by a high-level programming paradigm into the low execution level understood by the existing tools. Specifically, we extend the definition of vector clocks to allow the existing state-of-the-art race detectors to recognize those races that occur at the higher level of concurrency with minor modifications to these tools. Our evaluation with our prototype implemented within ThreadSanitizer shows that TLC can allow the existing tool to detect these races accurately with only small additional analysis overheads.

International audience; It has been shown that annotating Petri net unfoldings with time stamps allows for building distributed testers for distributed systems. However, the construction of the annotated unfolding of a distributed system currently remains a centralized task. In this paper we extend a distributed unfolding technique in order to annotate the resulting unfolding with time stamps. This allows for distributed construction of distributed testers for distributed systems.

The vector clock is a fundamental tool for tracking causality in distributed applications. Unfortunately, it does not scale well to large systems because each process needs to maintain a vector of size n, where n is the total number of processes in the system. To address this problem, we propose the encoding of the vector clock using prime numbers to use a single number to represent vector time. We propose the operations on the encoded vector clock (EVC). We then show how to timestamp global states and how to perform operations on the global states using the EVC. We also discuss scalability issues of the EVC.