Efficient Linearizability Checking for Actor-based Systems

• URL: http://arxiv.org/abs/2110.06407v2
• Date: Wed, 19 Jul 2023 17:15:45 GMT
• Title: Efficient Linearizability Checking for Actor-based Systems
• Authors: Mohammed S. Al-Mahfoudh and Ryan Stutsman and Ganesh Gopalakrishnan
• Abstract summary: We present our work on linearizability checking in DS2, an integrated framework for specifying, synthesizing, and testing distributed actor systems. DS2 automatically explores the concurrent schedules that system could arrive at, and it compares observed output of the system to ensure it is equivalent to what the sequential implementation could have produced.
• Score: 0.3157031081861668
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Recent demand for distributed software had led to a surge in popularity in actor-based frameworks. However, even with the stylized message passing model of actors, writing correct distributed software is still difficult. We present our work on linearizability checking in DS2, an integrated framework for specifying, synthesizing, and testing distributed actor systems. The key insight of our approach is that often subcomponents of distributed actor systems represent common algorithms or data structures (e.g.\ a distributed hash table or tree) that can be validated against a simple sequential model of the system. This makes it easy for developers to validate their concurrent actor systems without complex specifications. DS2 automatically explores the concurrent schedules that system could arrive at, and it compares observed output of the system to ensure it is equivalent to what the sequential implementation could have produced. We describe DS2's linearizability checking and test it on several concurrent replication algorithms from the literature. We explore in detail how different algorithms for enumerating the model schedule space fare in finding bugs in actor systems, and we present our own refinements on algorithms for exploring actor system schedules that we show are effective in finding bugs.

Related papers

• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQ is a new formulation for scene graph generation that avoids the multi-task learning problem and the entity pair distribution. We employ a DETR-based encoder-decoder conditional queries to significantly reduce the entity label space as well. Experimental results show that TraCQ not only outperforms existing single-stage scene graph generation methods, it also beats many state-of-the-art two-stage methods on the Visual Genome dataset.
  arXiv  Detail & Related papers  (2023-06-09T06:02:01Z)
• A Hierarchical Approach to Conditional Random Fields for System Anomaly Detection [0.8164433158925593]
  Anomaly detection to recognize unusual events in large scale systems is critical in many industries. A hierarchical approach takes advantage of the implicit relationships in complex systems and localized context.
  arXiv  Detail & Related papers  (2022-10-26T21:02:47Z)
• Learning to generate Reliable Broadcast Algorithms [10.77039660100327]
  This work presents an intelligent agent that uses Reinforcement Learning to generate correct and efficient fault-tolerant distributed algorithms. We show that our approach is able to generate correct fault-tolerant Reliable Broadcast algorithms with the same performance of others available in the literature, in only 12,000 learning episodes.
  arXiv  Detail & Related papers  (2022-07-31T21:45:20Z)
• Autoregressive Search Engines: Generating Substrings as Document Identifiers [53.0729058170278]
  Autoregressive language models are emerging as the de-facto standard for generating answers. Previous work has explored ways to partition the search space into hierarchical structures. In this work we propose an alternative that doesn't force any structure in the search space: using all ngrams in a passage as its possible identifiers.
  arXiv  Detail & Related papers  (2022-04-22T10:45:01Z)
• Activity Recognition in Assembly Tasks by Bayesian Filtering in Multi-Hypergraphs [1.2961180148172198]
  We study sensor-based human activity recognition in manual work processes like assembly tasks. In our approach, system states are represented by multi-hypergraphs, and the system dynamics is modeled by graph rewriting rules. We show a preliminary concept that allows to represent distributions over multi-hypergraphs more compactly than by full enumeration, and present an inference algorithm that works directly on this compact representation.
  arXiv  Detail & Related papers  (2022-02-01T11:01:09Z)
• CREPO: An Open Repository to Benchmark Credal Network Algorithms [78.79752265884109]
  Credal networks are imprecise probabilistic graphical models based on, so-called credal, sets of probability mass functions. A Java library called CREMA has been recently released to model, process and query credal networks. We present CREPO, an open repository of synthetic credal networks, provided together with the exact results of inference tasks on these models.
  arXiv  Detail & Related papers  (2021-05-10T07:31:59Z)
• MIST: Multiple Instance Self-Training Framework for Video Anomaly Detection [76.80153360498797]
  We develop a multiple instance self-training framework (MIST) to efficiently refine task-specific discriminative representations. MIST is composed of 1) a multiple instance pseudo label generator, which adapts a sparse continuous sampling strategy to produce more reliable clip-level pseudo labels, and 2) a self-guided attention boosted feature encoder. Our method performs comparably to or even better than existing supervised and weakly supervised methods, specifically obtaining a frame-level AUC 94.83% on ShanghaiTech.
  arXiv  Detail & Related papers  (2021-04-04T15:47:14Z)
• Distribution Alignment: A Unified Framework for Long-tail Visual Recognition [52.36728157779307]
  We propose a unified distribution alignment strategy for long-tail visual recognition. We then introduce a generalized re-weight method in the two-stage learning to balance the class prior. Our approach achieves the state-of-the-art results across all four recognition tasks with a simple and unified framework.
  arXiv  Detail & Related papers  (2021-03-30T14:09:53Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems. It combines deep learning and timed automata for creating behavioral model from observations. The algorithm has been applied to few data sets including two from real systems and has shown promising results.
  arXiv  Detail & Related papers  (2020-10-29T08:27:43Z)
• Controlled time series generation for automotive software-in-the-loop testing using GANs [0.5352699766206808]
  Testing automotive mechatronic systems partly uses the software-in-the-loop approach, where systematically covering inputs of the system-under-test remains a major challenge. One approach is to craft input sequences which eases control and feedback of the test process but falls short of exposing the system to realistic scenarios. The other is to replay sequences recorded from field operations which accounts for reality but requires collecting a well-labeled dataset of sufficient capacity for widespread use, which is expensive. This work applies the well-known unsupervised learning framework of Generative Adrial Networks (GAN) to learn an unlabeled dataset of recorded in-vehicle
  arXiv  Detail & Related papers  (2020-02-16T16:19:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.