Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs

• URL: http://arxiv.org/abs/2307.15930v1
• Date: Sat, 29 Jul 2023 08:43:49 GMT
• Title: Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
• Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer B{\o}nneland, Sarbojit Das, Bengt Jonsson, Magnus L{\aa}ng, and Konstantinos Sagonas
• Abstract summary: We present Event-DPOR, a DPOR algorithm tailored to event-driven programs. It is based on Optimal-DPOR, an optimal DPOR algorithm for multi-threaded programs. We prove correctness of Event-DPOR for all programs, and optimality for a large subclass.
• Score: 1.2948955292336792
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Event-driven multi-threaded programming is an important idiom for structuring concurrent computations. Stateless Model Checking (SMC) is an effective verification technique for multi-threaded programs, especially when coupled with Dynamic Partial Order Reduction (DPOR). Existing SMC techniques are often ineffective in handling event-driven programs, since they will typically explore all possible orderings of event processing, even when events do not conflict. We present Event-DPOR , a DPOR algorithm tailored to event-driven multi-threaded programs. It is based on Optimal-DPOR, an optimal DPOR algorithm for multi-threaded programs; we show how it can be extended for event-driven programs. We prove correctness of Event-DPOR for all programs, and optimality for a large subclass. One complication is that an operation in Event-DPOR, which checks for redundancy of new executions, is NP-hard, as we show in this paper; we address this by a sequence of inexpensive (but incomplete) tests which check for redundancy efficiently. Our implementation and experimental evaluation show that, in comparison with other tools in which handler threads are simulated using locks, Event-DPOR can be exponentially faster than other state-of-the-art DPOR algorithms on a variety of programs and manages to completely avoid unnecessary exploration of executions.

Related papers

• Grounding Partially-Defined Events in Multimodal Data [61.0063273919745]
  We introduce a multimodal formulation for partially-defined events and cast the extraction of these events as a three-stage span retrieval task. We propose a benchmark for this task, MultiVENT-G, that consists of 14.5 hours of densely annotated current event videos and 1,168 text documents, containing 22.8K labeled event-centric entities. Results illustrate the challenges that abstract event understanding poses and demonstrates promise in event-centric video-language systems.
  arXiv  Detail & Related papers  (2024-10-07T17:59:48Z)
• A Learning Support Method for Multi-threaded Programs Using Trace Tables [0.0]
  Multi-threaded programs are expected to improve responsiveness and conserve resources by dividing an application process into multiple threads for concurrent processing. However, due to scheduling and the interaction of multiple threads, their runtime behavior is more complex than that of single-threaded programs. We propose a learning tool for multi-threaded programs using trace tables.
  arXiv  Detail & Related papers  (2024-09-25T07:46:38Z)
• Event-ECC: Asynchronous Tracking of Events with Continuous Optimization [1.9446776999250501]
  We propose a tracking algorithm that computes a 2D motion warp per single event, called event-ECC (eECC) The computational burden of event-wise processing is alleviated through a lightweight version that benefits from incremental processing and updating scheme. We report improvements in tracking accuracy and feature age over state-of-the-art event-based asynchronous trackers.
  arXiv  Detail & Related papers  (2024-09-22T19:03:19Z)
• Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
  We present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption.
  arXiv  Detail & Related papers  (2024-05-18T00:07:26Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC) is a novel fact-checking model that decomposes complex claims into simpler sub-tasks. We first leverage the in-context learning ability of large language models to generate reasoning programs. We execute the program by delegating each sub-task to the corresponding sub-task handler.
  arXiv  Detail & Related papers  (2023-05-22T06:11:15Z)
• Unifying Event Detection and Captioning as Sequence Generation via Pre-Training [53.613265415703815]
  We propose a unified pre-training and fine-tuning framework to enhance the inter-task association between event detection and captioning. Our model outperforms the state-of-the-art methods, and can be further boosted when pre-trained on extra large-scale video-text data.
  arXiv  Detail & Related papers  (2022-07-18T14:18:13Z)
• Modeling Continuous Time Sequences with Intermittent Observations using Marked Temporal Point Processes [25.074394338483575]
  A large fraction of data generated via human activities can be represented as a sequence of events over a continuous-time. Deep learning models over these continuous-time event sequences is a non-trivial task. In this work, we provide a novel unsupervised model and inference method for learning MTPP in presence of event sequences with missing events.
  arXiv  Detail & Related papers  (2022-06-23T18:23:20Z)
• What Averages Do Not Tell -- Predicting Real Life Processes with Sequential Deep Learning [0.1376408511310322]
  Process Mining concerns discovering insights on business processes from their execution data that are logged by systems. Many Deep Learning techniques have been successfully adapted for predictive Process Mining that aims to predict process outcomes. Traces in Process Mining are multimodal sequences and very differently structured than natural language sentences or images.
  arXiv  Detail & Related papers  (2021-10-19T19:45:05Z)
• Process Discovery for Structured Program Synthesis [70.29027202357385]
  A core task in process mining is process discovery which aims to learn an accurate process model from event log data. In this paper, we propose to use (block-) structured programs directly as target process models. We develop a novel bottom-up agglomerative approach to the discovery of such structured program process models.
  arXiv  Detail & Related papers  (2020-08-13T10:33:10Z)
• Team RUC_AIM3 Technical Report at Activitynet 2020 Task 2: Exploring Sequential Events Detection for Dense Video Captioning [63.91369308085091]
  We propose a novel and simple model for event sequence generation and explore temporal relationships of the event sequence in the video. The proposed model omits inefficient two-stage proposal generation and directly generates event boundaries conditioned on bi-directional temporal dependency in one pass. The overall system achieves state-of-the-art performance on the dense-captioning events in video task with 9.894 METEOR score on the challenge testing set.
  arXiv  Detail & Related papers  (2020-06-14T13:21:37Z)
• Dynamic Multi-Robot Task Allocation under Uncertainty and Temporal Constraints [52.58352707495122]
  We present a multi-robot allocation algorithm that decouples the key computational challenges of sequential decision-making under uncertainty and multi-agent coordination. We validate our results over a wide range of simulations on two distinct domains: multi-arm conveyor belt pick-and-place and multi-drone delivery dispatch in a city.
  arXiv  Detail & Related papers  (2020-05-27T01:10:41Z)

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.