This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model finegrained behaviors of ZooKeeper and use the TLC model checker to verify its correctness properties; we also check conformance between the model and code. The fundamental challenge is to balance the granularity of specifications and the scalability of model checking---fine-grained specifications lead to state-space explosion, while coarse-grained specifications introduce model-code gaps. To address this challenge, we write specifications with different granularities for composable modules, and compose them into mixed-grained specifications based on specific scenarios. For example, to verify code changes, we compose fine-grained specifications of changed modules and coarse-grained specifications that abstract away details of unchanged code with preserved interactions. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space, especially for evolving software where changes are typically local and incremental. We detected six severe bugs that violate five types of invariants and verified their code fixes; the fixes have been merged to ZooKeeper. We also improve the protocol design to make it easy to implement correctly.

Burckhardt et al. proposed a formal specification framework for eventually consistent replicated data types, denoted$(vis, ar)$, based on the notions of visibility and arbitration relations. However, being specific to eventually consistent systems, this framework has two limitations. First, it does not cover non-convergent consistency models since arbitration$ar$is a total order over events. Second, it does not cover the consistency models in which each event is required to be aware of the return values of some events that are visible to it when justifying its return value. These limitations make the$(vis, ar)$framework not generic enough to specify and reason about important weak consistency models such as Causal Memory and PRAM. In this article, we extend this framework to a more generic one called$(vis, ar, V)$for weakly consistent replicated data types. To specify non-convergent consistency models as well, we relax the arbitration relation$ar$to be a partial order. To overcome the second limitation, we allow to specify for each event$e$, a subset$V(e)$of its visible set whose return values cannot be ignored when justifying the return value of$e$. To make it practically feasible, we provide candidates for the visibility and arbitration relations and the$V$function. By combining candidates for these three components, we are able to specify not only existing consistency models but also new ones that are reasonable and promising for practical usefulness. We then show how to specify consistency models in our framework, and provide three case studies.

Implementation-level distributed system model checkers (DMCKs) have proven valuable in verifying the correctness of real distributed systems. However, they primarily focus on state space reduction, and often have a bottleneck on another crucial dimension: exploration speed. To scale DMCK, we introduce SandTable, a technique for lifting state-space exploration from the implementation level to the specification level, and confirming bugs at the implementation level. We made SandTable practical through a methodology consisting of four essential parts: (1) writing specifications that adhere to the implementation, (2) checking conformance to enhance specification quality and reduce false positives and false negatives, (3) exploring the state space with heuristics for effectiveness and efficiency, and (4) confirming bugs and verifying their fixes in the implementation.

Abstract Internet‐scale distributed systems often replicate data at multiple geographic locations to provide low latency and high availability, despite node and network failures. According to the CAP theorem, low latency and high availability can only be achieved at the cost of accepting weak consistency. The conflict‐free replicated data type (CRDT) is a framework that provides a principled approach to maintaining eventual consistency among data replicas. CRDTs have been notoriously difficult to design and implement correctly. Subtle deep bugs lie in the complex and tedious handling of all possible cases of conflicting data updates. We argue that the CRDT design should be formally specified and model checked, to uncover deep bugs which are beyond human reasoning. The implementation further needs to be systematically tested. On the one hand, the testing needs to inherit the exhaustive nature of the model checking and ensures the coverage of testing. On the other hand, the testing is expected to find coding errors which cannot be detected by design level verification. Toward the challenges above, we propose the model‐checking‐driven explorative testing ( MET ) framework. At the design level, MET uses TLA+ to specify and model check CRDT designs. At the implementation level, MET conducts model‐checking‐driven explorative testing, in the sense that the test cases are automatically generated from the model‐checking traces. The system execution is controlled to proceed deterministically, following the model‐checking trace. The explorative testing systematically controls and permutes all nondeterministic choices of message reorderings. We apply MET in our practical development of CRDTs. The bugs in both designs and implementations of CRDTs are found. As for bugs which can be found by traditional testing techniques, MET greatly reduces the cost of fixing the bugs. Moreover, MET can find subtle deep bugs which cannot be found by existing techniques at a reasonable cost. Based on our practical use of MET , we discuss how MET provides us with sufficient confidence in the correctness of our CRDT designs and implementations. Conflict‐free replicated data type (CRDT) is a framework that provides a principled approach to maintaining eventual consistency among data replicas in distributed systems. CRDTs have been notoriously difficult to design and implement correctly. We propose model‐checking‐driven explorative testing ( MET ) framework for dealing with such problem. We apply MET in our practical development of CRDTs. MET successfully finds subtle deep bugs and provides us with sufficient confidence in the correctness of our CRDT designs and implementations.

Internet-scale distributed systems often rely on replication to achieve fault-tolerance and load distribution. To provide low latency and high availability, the systems are often required to accept updates on one replica immediately and then propagate the updates among replicas asynchronously. Conflict-free Replicated Data Type (CRDT) is a principled approach to addressing the challenge for these systems to resolve conflicts among concurrent updates. Although many CRDTs have been studied, little research has been done on Conflict-free Replicated Priority Queue (CRPQ), which is a collection of elements that focuses on maintaining element orderings based on their priority values, and can be used in many applications scenarios such as task scheduling and network routing. In this work, we discuss the design rationales of CRPQs and introduce two CRPQ designs: Add-Win CRPQ and Remove-Win CRPQ. The correctness of the designs is formally verified using TLA+. We also demonstrate the effectiveness of our designs by implementing them over Redis. Our evaluation shows that both CRPQs perform well in terms of data consistency and memory overhead.

To achieve high availability and low latency, dis-tributed data stores often geographically replicate data at multiple sites called replicas. However, this introduces the data consistency problem. Due to the fundamental tradeoffs among consistency, availability, and latency in the presence of network partition, no a one-size-fits-all consistency model exists. To meet the needs of different applications, many popular data stores provide tunable consistency, allowing clients to specify the consistency level per individual operation. In this paper, we propose tunable causal consistency (TCC). It allows clients to choose the desired session guarantee for each operation, from the well-known four session guarantees, i.e., read your writes, monotonic reads, monotonic writes, and writes follow reads. Specifically, we first propose a formal specffication of TCC in an extended (vis, ar) framework originally proposed by Burckhardt et al. Then we design a TCC protocol and develop a prototype distributed key-value store called TCCSTORE. We evaluate TCCSTORE on Aliyun. The latency is less than 38ms for all workloads and the throughput is up to about 1900 operations per second. We also show that TCC achieves better performance than causal consistency and requires a negligible overhead when compared with eventual consistency.

Consensus protocols are widely used in building reliable distributed software systems and their correctness is of vital importance. TLA+ is a lightweight formal specification language which enables precise specification of system design and exhaustive checking of the design without any human effort. The features of TLA+ make it widely used in the specification and model checking of consensus protocols, both in academia and in industry. However, the application of TLA+ is limited by the state explosion problem in model checking. Though compositional model checking is essential to tame the state explosion problem, existing compositional checking techniques do not sufficiently consider the characteristics of TLA+. In this work, we propose the Interaction-Preserving Abstraction (IPA) framework, which leverages the features of TLA+ and enables practical and efficient compositional model checking of consensus protocols specified in TLA+. In the IPA framework, system specification is partitioned into multiple modules, and each module is divided into the internal part and the interaction part. The basic idea of the interaction-preserving abstraction is to omit the internal part of each module, such that another module cannot distinguish whether it is interacting with the original module or the coarsened abstract one. We apply the IPA framework to the compositional checking of the TLA+ specifications of two consensus protocols Raft and ParallelRaft. Raft is a consensus protocol which was originally developed in academia and then widely used in industry. ParallelRaft is the replication protocol in PolarFS, the distributed file system for the commercial database Alibaba PolarDB. We demonstrate that the IPA framework is easy to use in realistic scenarios and at the same time significantly reduces the model checking cost.

Distributed storage systems employ replication to improve performance and reliability. To provide low latency data access, replicas are often required to accept updates without coordination with each other, and the updates are then propagated asynchronously. This brings the critical challenge of conflict resolution among concurrent updates. Conflict-free Replicated Data Type (CRDT) is a principled approach to addressing this challenge. However, existing CRDT designs are tricky, and hard to be generalized to other data types. A design framework is in great need to guide the systematic design of new CRDTs. To address this challenge, we propose RWF - the Remove-Win design Framewerk for CRDTs. RWF leverages the simple but powerful remove-win strategy to resolve conflicting updates, and provides generic design for a variety of data container types. Two exemplar implementations following RWF are given over the Redis data type store, which demonstrate the effectiveness of RWF. Performance measurements of our implementations further show the efficiency of CRDT designs following RWF.

Although it has been commercially successful to deploy weakly consistent but highly-responsive distributed datastores, the tension between developing complex applications and obtaining only weak consistency guarantees becomes more and more severe. The almost strong consistency tradeoff aims at achieving both strong consistency and low latency in the common case. In distributed storage systems, we investigate the generic notion of almost strong consistency in terms of designing fast read algorithms while guaranteeing Probabilistic Atomicity with well-Bounded staleness (PAB). This problem has been explored in the case where only one client can write the data. However, the more general case where multiple clients can write the data has not been studied. In this article, we study the fast read algorithm for PAB in the multi-writer case. We show the bound of data staleness and the probability of atomicity violation by decomposing inconsistent reads into the read inversion and the write inversion patterns. We implement the fast read algorithm and evaluate the consistency-latency tradeoffs based on the instrumentation of Cassandra and the YCSB benchmark framework. The theoretical analysis and the experimental evaluations show that our fast read algorithm guarantees PAB, even when faced with dynamic changes in the computing environment.

MongoDB is one of the first commercial distributed databases that support causal consistency. Its implementation of causal consistency combines several research ideas for achieving scalability, fault tolerance, and security. Given its inherent complexity, a natural question arises: Has MongoDB correctly implemented causal consistency as it claimed?

Distributed multi-writer atomic registers are at the heart of a large number of distributed algorithms. While enjoying the benefits of atomicity, researchers further explore fast implementations of atomic reigsters which are optimal in terms of data access latency. Though it is proved that multi-writer atomic register implementations are impossible when both read and write are required to be fast, it is still open whether implementations are impossible when only write or read is required to be fast. This work proves the impossibility of fast write implementations based on a series of chain arguments among indistiguishable executions. We also show the necessary and sufficient condition for fast read implementations by extending the results in the single-writer case. This work concludes a series of studies on fast implementations of distributed atomic registers.

Recently Burckhardt et al. proposed a formal specification framework for eventually consistent replicated data types, denoted (vis, ar), based on the notions of visibility and arbitration relations. However, being specific to eventually consistent systems, this framework has two limitations. First, it does not cover non-convergent consistency models since arbitration ar is defined to be a total order over events in a computation. Second, it does not cover the consistency models in which each event is required to be aware of the return values of some or all events that are visible to it.In this paper, we extend the (vis, ar) specification framework into a more generic one called (vis, ar, V) for weakly consistent replicated data types. To specify non-convergent consistency models as well, we simply relax the arbitration relation ar to be a partial order. To overcome the second limitation, we allow to specify for each event e, a subset V(e) of its visible set whose return values cannot be ignored when justifying the return value of e. To make it practically feasible, we provide candidates for the visibility and arbitration relations and the V function. By combining these candidates, we demonstrate how to specify various existing consistency models in the (vis, ar, V) framework. Moreover, it helps to discover new consistency models. As a case study, we prove that the causal consistency protocol of MongoDB database satisfies Causal Memory Convergence, a new causal consistency variant discovered in our framework.

The replicated list object is frequently used to model the core functionality of replicated collaborative text editing systems. Since 1989, the convergence property has been a common specification of a replicated list object. Recently, Attiya et al. proposed the strong/weak list specification and conjectured that the well-known Jupiter protocol satisfies the weak list specification. The major obstacle to proving this conjecture is the mismatch between the global property on all replica states prescribed by the specification and the local view each replica maintains in Jupiter using data structures like 1D buffer or 2D state space. To address this issue, we propose CJupiter (Compact Jupiter) based on a novel data structure called $n$-ary ordered state space for a replicated client/server system with $n$ clients. At a high level, CJupiter maintains only a single $n$-ary ordered state space which encompasses exactly all states of each replica. We prove that CJupiter and Jupiter are equivalent and that CJupiter satisfies the weak list specification, thus solving the conjecture above.

The replicated list object is frequently used to model the core functionality of replicated collaborative text editing systems. Recently, Attiya et al. proposed the strong/weak list specification and conjectured that the well-known Jupiter protocol satisfies the weak list specification. The major obstacle to proving this conjecture is the mismatch between the global property on all replica states prescribed by the specification and the local view each replica maintains in Jupiter using data structures like 1D buffer or 2D state space. To address this issue, we propose CJupiter (Compact Jupiter) based on a novel data structure called n-ary ordered state space for a replicated client/server system with n clients. At a high level, CJupiter maintains only a single n-ary ordered state space which encompasses exactly all states of each replica. We prove that CJupiter and Jupiter are equivalent and that CJupiter satisfies the weak list specification, thus solving the conjecture above.

Flash-based Solid State Drive (SSD) is widely used in the virtualization environment, usually as the cache of the hard disk drive-based Virtual Machine (VM) storage, to improve the IO performance. Existing SSD caching schemes are mainly driven by VM-centric metrics. They treat the VMs as independent units and focus on critical low-level performance metrics of individual VMs, such as the working set, the IO latency, or the throughput. However, for elastic Hadoop applications consisting of multiple VMs, the workload is rapidly changing, and the importance of differnet VMs may be different even if they have the same low-level IO pattern. In this situation, the VM-centric SSD caching schemes may not lead to the best performance, i.e., the shortest job completion time. Considering the importance of VMs and relationships among VMs inside the application may potentially better improve the performance, which we regard as the application-centric metrics. We propose the Application-Centric SSD caching for Hadoop applications (ACSSD), which reduces the job completion time from the application level. AC-SSD uses the genetic algorithm based approach to calculate the nearly optimal weights of virtual machines for allocating SSD cache space and controlling the I/O Operations Per Second (IOPS) based on the importance of the VMs. Moreover, AC-SSD introduces the closed-loop adaptation to face the rapidly changing workload. The evaluation shows that AC-SSD reduces the job completion time by up to 39% for IO sensitive workloads, and up to 29% for rapidly changing workloads.

Several relaxed variants of Snapshot Isolation (SI) have been proposed for improved performance in distributed transactional key-value stores. These relaxed variants, however, provide no specification or control of the severity of the anomalies with respect to SI. They have also been designed to be used statically throughout the whole system life cycle. To overcome these drawbacks, we propose the idea of parameterized and runtime-tunable snapshot isolation. We first define a new transactional consistency model called Relaxed Version Snapshot Isolation (RVSI), which can formally and quantitatively specify the anomalies it may produce with respect to SI. To this end, we decompose SI into three "view properties", for each of which we introduce a parameter to quantify one of three kinds of possible anomalies: k1-BV (k1-version bounded backward view), k2-FV (k2-version bounded forward view), and k3-SV (k3-version bounded snapshot view). We then implement a prototype partitioned replicated distributed transactional key-value store called Chameleon across multiple data centers. While achieving RVSI, Chameleon allows each transaction to dynamically tune its consistency level at runtime. The experiments show that RVSI helps to reduce the transaction abort rates when applications are willing to tolerate certain anomalies. We also evaluate the individual impacts of k1-BV, k2-FV, and k3-SV on reducing the transaction abort rates in various scenarios. We find that it depends on the issue delays between clients and replicas which of k1 and k2 plays a major role in reducing transaction abort rates.

A consistency/latency tradeoff arises as soon as a distributed storage system replicates data. For low latency, distributed storage systems often settle for weak consistency conditions, providing little guarantee on data consistency. In this paper, we propose the notion of almost strong consistency as an option for the consistency/latency tradeoff. It provides both deterministically bounded staleness of data versions for reads and probabilistic quantification on the rate of “reading stale data”, while achieving low latency. We then investigate almost strong consistency in terms of probabilistically-atomic 2-atomicity. Our PA2AM algorithm for the single-writer model completes each read in one communication round-trip, and guarantees that each read obtains the value of within the latest two versions. To quantify the rate of “reading the stale version”, we decompose the so-called “old-new inversion” anomaly into long-lived write concurrency patterns and non-monotonic read-write patterns, and propose a queueing model and a timed balls-into-bins model to analyze them, respectively. The probabilistic analysis not only demonstrates that old-new inversions rarely occur, but also reveals that the read-write pattern dominates in preventing them from occurring. These are then supported by our experiments. To further demonstrate the benefits of probabilistically-atomic 2-atomicity, we also compare it to weak consistency conditions.

Distributed shared memory-based coordination has the advantage of simplifying the coordination logic to read/write operations over the illusionary local memory. However, it is notoriously challenging to come up with a cost-effective implementation of the distributed shared memory. The implementation becomes more challenging in mobile environments, due to the resource constraints and the more rapid changes in the computing context. To this end, we propose the Mobile Distributed Shared Memory (MDSM) middleware to facilitate the development of mobile coordination applications. The key constructs in the shared memory are shared registers. Shared registers with different read/write patterns are implemented to facilitate flexible coordination. The registers also have different consistency semantics, to enable efficient tradeoff between data consistency and data access cost. An application framework is proposed to simplify the implementation of mobile coordination, relying on the middleware support from MDSM. A case study is conducted to demonstrate the usage of MDSM, where a soccer game application for the mobile phone is developed. Experimental evaluation is conducted to quantify different options of the consistency-latency tradeoff in the case study. The performance measurements show the cost-effectiveness of eventual consistency in this game. We also verify the read/write traces to further explain why eventual consistency practically performs better than it can guarantee.

Pervasive applications are involving more and more autonomous computing and communicating devices, augmented with the abilities of sensing and controlling the logical/physical environment. To enable context-awareness for such applications, we are challenged by the intrinsic asynchrony of the computing environment. Predicate detection is a well studied technique dedicated to detecting global predicates over asynchronous computations and can be employed to achieve context-awareness of the asynchronous environment. However, there is no methodological framework which guides us to systematically apply the abstract predicate detection theory to the development of concrete context-aware applications. To this end, we present the Predicate Detection-based ContextAwareness (PD-CA) framework. PD-CA maps the concepts of context-awareness to concepts of predicate detection. PD-CA also presents a design process of providing middleware support for context-aware applications. Under the guidance of the PD-CA framework, we design and implement the Middleware Infrastructure for Predicate detection in Asynchronous environments (MIPA). We also propose the programming toolkit to facilitate the development of context-aware applications based on MIPA, and demonstrate the use of the toolkit by a case study of a chemical plant safety management application. Experimental evaluations show the performance of MIPA in enabling context-awareness despite of the asynchrony.

Data replication technologies in distributed storage systems introduce the problem of data consistency. For high performance, data replication systems often settle for weak consistency models, such as Pipelined-RAM consistency. To determine whether a data replication system provides Pipelined-RAM consistency, we study the problem ofverifying Pipelined-RAM consistencyover read/write traces (VPC, for short). Four variants of VPC (labeled VPC-SU, VPC-MU, VPC-SD, and VPC-MD) are identified according to whether there are Multiple shared variables (or one Single variable) and whether write operations can assign Duplicate values (or only Unique values) to each shared variable. We prove that VPC-SD is$\sf {NP}$-complete (so is VPC-MD) by reducing the strongly$\sf {NP}$-complete problem3-Partitionto it. For VPC-MU, we present theRead-Centricalgorithm with time complexity$O(n^4)$, where$n$is the number of operations. The algorithm constructs an operation graph by iteratively applying a rule which guarantees that no overwritten values can be read later. It incrementally processes all the read operations one by one, and exploits the total order between the dictating writes on the same variable to avoid redundant applications of the rule. The experiments have demonstrated its practical efficiency and scalability.

Coordinating mobile robots are widely used in commercial and industrial settings to fulfill various tasks. However, to program the coordination among mobile robots is challenging. A coordination framework is needed to shield the programmer from handling low-level details of robot control and communication, while supporting flexible and cost-effective coordination at the same time. The coordination framework should also be able to well coexist with the underlying robot control. To this end, we propose the Coordination-enabled Behavior-Based Robotics (CBBR) framework. CBBR employs Distributed Shared Memory (DSM) to support coordination. The shared memory illusion built by the DSM greatly simplifies the coordination logic. Moreover, the flexible access patterns of the DSM and the rich consistency semantics of the DSM reads and writes enable flexible and cost-effective coordination.

The event stream model of computation has a wide range of applications, e.g, computer system monitoring, physical environment sensing/surveillance, and stock trade monitoring. Sliding windows are widely used to facilitate effective event stream processing. However, it is greatly challenged when the event sources are distributed and asynchronous. One important technique to cope with the asynchrony is to utilize that the meaningful snapshots of an asynchronous computation form a distributive lattice. It thus becomes the central challenge whether this lattice structure still preserves and how to maintain it at runtime, when we restrict our attention to events within sliding windows. To address this challenge, we first prove that the snapshots of the asynchronous event streams within the sliding windows form a convex distributive lattice (denoted by Lat-Win). This enables us to easily integrate existing predicate specification and detection techniques, to express and monitor properties of our concern over asynchronous event streams. Then we propose an algorithm to maintain Lat-Win at runtime. The proposed scheme is evaluated in a context-aware smart office scenario, where activities of the user can be recognized by monitoring multiple streams of sensed events. The Lat-Win algorithm is implemented on the open-source context-aware middleware we developed. The evaluation results first show the advantage of adopting sliding windows over asynchronous event streams. Then they show the performance of detecting specified predicates within Lat-Win, with dynamic changes in the computing environment.

Formal specification and runtime detection of contextual properties is one of the primary approaches to enabling context awareness in pervasive computing environments. Due to the intrinsic dynamism of the pervasive computing environment, dynamic properties, which delineate concerns of context-aware applications on the temporal evolution of the environment state, are of great importance. However, detection of dynamic properties is challenging, mainly due to the intrinsic asynchrony among computing entities in the pervasive computing environment. Moreover, the detection must be conducted at runtime in pervasive computing scenarios, which makes existing schemes do not work. To address these challenges, we propose the property detection for asynchronous context (PDAC) framework, which consists of three essential parts: 1) Logical time is employed to model the temporal evolution of environment state as a lattice. The active surface of the lattice is introduced as the key notion to model the runtime evolution of the environment state; 2) Specification of dynamic properties is viewed as a formal language defined over the trace of environment state evolution; and 3) The SurfMaint algorithm is proposed to achieve runtime maintenance of the active surface of the lattice, which further enables runtime detection of dynamic properties. A case study is conducted to demonstrate how the PDAC framework enables context awareness in asynchronous pervasive computing scenarios. The SurfMaint algorithm is implemented and evaluated over MIPA--the open-source context-aware middleware we developed. Performance measurements show the accuracy and cost-effectiveness of SurfMaint, even when faced with dynamic changes in the asynchronous pervasive computing environment.

Efficient detection of RFID-tagged physical objects is one of the key enabling technologies to build pervasive Internet-of-Things applications. However, the detection of tagged-objects is faced with the critical challenge of tag dynamics, which mainly arises from the movement of tagged physical objects. To capture tag dynamics, the application needs to detect the presence/absence of tags in an accurate, timely and cost-effective way. To address these challenges, we propose the Prediction of Tag Dynamics (PTD) algorithm. PTD achieves runtime detection of tagged-objects by i) streaming of the temporally-correlated tag readings obtained from persistent tracking of the tagged-object, and ii) runtime prediction of tag dynamics based on the streaming of tag readings. The performance of PTD is investigated based on real implementation and experimental evaluation, where PTD processes tag readings gathered with high fidelity from persistent tracking of real activities of tagged objects. The evaluation results demonstrate the accuracy, timeliness and cost-effectiveness of PTD.

Formal specification and runtime detection of temporal properties for pervasive context is one of the primary approaches to achieving context-awareness. Though temporal logics have been widely used in specification of temporal properties, they are faced with severe challenges in Pervasive Computing (PvC) scenarios. First, temporal logics are traditionally defined over infinite traces of possible system behavior. However in PvC scenarios, applications observe finite prefixes of (potentially infinite) traces of environment state evolution, and adapt their behavior accordingly. Second, specification and detection of temporal properties are challenged by the intrinsic asynchrony of PvC environments. Discussions above necessitate a systematic approach to formal specification and runtime detection of temporal properties for asynchronous context. To this end, we propose CTL3(3-valued Computation Tree Logic), which i) adopts 3-valued semantics to capture the inconclusiveness when applications only observe finite prefixes of environment state evolution; ii) inherits the notion of branching time to capture the uncertainty resulting from the asynchrony of PvC environments. A case study is conducted to demonstrate how CTL3supports context-awareness in PvC scenarios. The runtime checking algorithm of CTL3is implemented and evaluated over MIPA - the open-source context-aware middle-ware we developed. The case study demonstrates the necessity of adopting CTL3in PvC scenarios, while the performance measurements show the cost-effectiveness of runtime checking contextual properties in CTL3.

Runtime detection of contextual properties is one of the primary approaches to enabling context-awareness in pervasive computing scenarios. Among various properties the applications may specify, the concurrency property, i.e., property delineating concurrency among contextual activities, is of great importance. It is because the concurrency property is one of the most frequently specified properties by context-aware applications. Moreover, the concurrency property serves as the basis for specification of many other properties. Existing schemes implicitly assume that context collecting devices share the same notion of time. Thus, the concurrency property can be easily detected. However, this assumption does not necessarily hold in pervasive computing environments, which are characterized by the asynchronous coordination among heterogeneous computing entities. To cope with this challenge, we identify and address three essential issues. First, we introduce logical time to model behavior of the asynchronous pervasive computing environment. Second, we propose the logic for specification of the concurrency property. Third, we propose the Concurrent contextual Activity Detection in Asynchronous environments (CADA) algorithm, which achieves runtime detection of the concurrency property. Performance analysis and experimental evaluation show that CADA effectively detects the concurrency property in asynchronous pervasive computing scenarios.

Context-awareness is an essential feature of pervasive applications, and runtime detection of contextual properties is one of the primary approaches to enabling context awareness. However, existing context-aware middleware does not provide sufficient support for detection of contextual properties in asynchronous environments. We argue that in asynchronous environments, the concept of time needs to be reexamined. Instead of assuming the availability of global time or synchronous interaction, we should rely on logical time. To this end, we present the Middleware Infrastructure for Predicate detection in Asynchronous environments (MIPA), which supports context-awareness based on logical time. Design and operation of MIPA are explained in detail. We also evaluate MIPA with a comprehensive case study. The evaluation results show the cost-effectiveness and scalability of MIPA.

Detection of contextual properties is one of the primary approaches to enabling context-awareness. In order to adapt to temporal evolution of the pervasive computing environment, context-aware applications often need to detect behavioral properties specified over the contexts. This problem is challenging mainly due to the intrinsic asynchrony of pervasive computing environments. However, existing schemes implicitly assume the availability of a global clock or synchronous coordination, thus not working in asynchronous environments. We argue that in pervasive computing environments, the concept of time needs to be reexamined. Toward this objective, we propose the Ordering Global Activity (OGA) algorithm, which detects behavioral contextual properties in asynchronous environments. The essence of our approach is to utilize the message causality and its on-the-fly coding as logical vector clocks. The OGA algorithm is implemented and evaluated based on the open-source context-aware middleware MIPA. The evaluation results show the impact of asynchrony on the detection of contextual properties, which justifies the primary motivation of our work. They also show that OGA can achieve accurate detection of contextual properties in dynamic pervasive computing environments.

One of the major applications of wireless ad hoc networks is to extend the Internet coverage and support pervasive and efficient data dissemination and sharing. To reduce data access cost and delay, caching has been widely used as an important technique. The efficiency of data access in caching systems largely depends on the cost for maintaining cache consistency, which can be high in wireless ad hoc networks due to network dynamism. Therefore, to make better trade-off between cache consistency and the cost incurred, it would be highly desirable to provide users the flexibility in specifying consistency requirements for their applications. In this paper, we propose a general consistency model called Probabilistic Delta Consistency (PDC), which integrates the flexibility granted by existing consistency models, covering them as special cases. We also propose the Flexible Combination of Push and Pull (FCPP) algorithm which satisfies user-specified consistency requirements under the PDC model. The analytical model of FCPP is used to derive the balance of minimizing the consistency maintenance cost and ensuring the specified consistency requirement. Extensive simulations are conducted to evaluate whether FCPP can satisfy arbitrarily specified consistency requirements, and whether FCPP works cost-effectively in dynamic wireless ad hoc networks. The evaluation results show that FCPP can adaptively tune itself to satisfy various user-specified consistency requirements. Moreover, it can save the traffic cost by up to 50 percent and reduce the query delay by up to 40 percent, compared with the widely used Pull with TTR algorithm.

Abstract Cooperative caching is an important technique to support pervasive Internet access. In order to ensure valid data access, the cache consistency must be maintained properly. However, this problem has not been sufficiently studied in mobile computing environments, especially those with ad hoc networks. There are two essential issues in cache consistency maintenance: consistency control initiation and data update propagation. Consistency control initiation not only decides the cache consistency provided to the users, but also impacts the consistency maintenance cost. This issue becomes more challenging in asynchronous and fully distributed ad hoc networks. To this end, we propose the predictive consistency control initiation (PCCI) algorithm, which adaptively initiates consistency control based on its online predictions of forthcoming data updates and cache queries. In order to efficiently propagate data updates through multi‐hop wireless connections, the hierarchical data update propagation (HDUP) algorithm is proposed. Theoretical analysis shows that cooperation among the caching nodes facilitates data update propagation. Extensive simulations are conducted to evaluate performance of both PCCI and HDUP. Evaluation results show that PCCI cost‐effectively initiates consistency control even when faced with dynamic changes in data update rate, cache query rate, node speed, and number of caching nodes. The evaluation results also show that HDUP saves cost for data update propagation by up to 66%. Copyright © 2009 John Wiley & Sons, Ltd.

Internetware is envisioned as a new software paradigm for resource integration and sharing in the open, dynamic and autonomous network environment. In this paper we discuss our visions and explorations of this new paradigm, with focus placed on the methodological perspective. A set of enabling techniques on flexible coordination of autonomous services, automatic adaptation to changing environment and trust management-based assurance of dependability are proposed to help the development of Internetware applications.

Contexts, the pieces of information that capture the characteristics of computing environments, are often inconsistent in the dynamic and uncertain pervasive computing environments. Various schemes have been proposed to check context consistency for pervasive applications. However, existing schemes implicitly assume that the contexts being checked belong to the same snapshot of time. This limitation makes existing schemes do not work in pervasive computing environments, which are characterized by the asynchronous coordination among computing devices. The main challenge imposed on context consistency checking by asynchronous environments is how to interpret and detect concurrent events. To this end, we propose in this paper the concurrent events detection for asynchronous consistency checking (CEDA) algorithm. An analytical model, together with corresponding numerical results, is derived to study the performance of CEDA. We also conduct extensive experimental evaluation to investigate whether CEDA is desirable for context-aware applications. Both theoretical analysis and experimental evaluation show that CEDA accurately detects concurrent events in time in asynchronous pervasive computing environments, even with dynamic changes in message delay, duration of events and error rate of context collection.

Context-awareness is a key issue in pervasive computing. Context-aware applications are prone to the context consistency problem, where applications are confronted with conflicting contexts and cannot decide how to adapt themselves. In pervasive computing environments, users are often willing to accept certain degree of context inconsistency, as long as it can reduce the consistency maintenance cost, e.g., query delay and battery power. However, existing consistency maintenance schemes do not enable the users to make such tradeoffs. To this end, we propose the probabilistic consistency checking for pervasive context (PCCPC) algorithm. Detailed performance analysis shows that PCCPC enables the users to check consistency over arbitrarily specified ratio of context. We also conduct experiments to study the cost reduced by probabilistic checking. The analytical and the experimental results show that PCCPC enables the users to efficiently make tradeoffs between context consistency and the associated checking cost.

Caching is an important technique to support pervasive Internet access. Cache consistency measures the deviation between the cached data and the source data. In mobile computing environments, especially with ad hoc networks, users are in great need of the flexibility in tuning their consistency requirements, in order to make tradeoffs between the specified cache consistency and the cost incurred. Existing works have used delta consistency (DC) and probabilistic consistency (PC) which, to some extent, provide the users with such flexibility. In this paper, we propose a general consistency model called probabilistic delta consistency (PDC). PDC covers all existing consistency models including DC and PC, and integrates the flexibility granted by both DC and PC. Thus, PDC enables the users to flexibly specify their consistency requirements in two orthogonal dimensions, namely the deviation in time/value and the ratio of queries gaining the specified consistency. We also propose a consistency maintenance algorithm, called flexible combination of push and pull (FCPP), which can meet users' consistency requirements specified under the PDC model. An analytical model is derived to achieve the optimized combination of push and pull, so as to ensure the user-specified consistency requirements, while minimizing the consistency maintenance overhead. Extensive simulations are conducted to evaluate the performance of the FCPP algorithm. Evaluation results show that, compared with the widely used dynamic TTR algorithm, FCPP can save up to 68% of the traffic overhead and reduce the query delay by up to 84%

Peer-to-peer computing is mainly based on the virtual overlay network constructed in the application layer. Often, there is topology mismatching between the overlay network and the physical network, which may cause great traffic overhead. In this paper, we study the topology mismatching problem and its impact on communication in wireless ad hoc networks. We present an efficient, fully distributed algorithm, named D-TAOC, for constructing the overlay network. By qualitative analysis and simulation experiments, we show that D-TAOC can significantly reduce the traffic overhead while slightly sacrificing the routing efficiency. We also prove that D-TAOC works well in a dynamic peer-to-peer environment.