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
- SEED: Accelerating Reasoning Tree Construction via Scheduled Speculative Decoding [16.380389806465733]
Large Language Models (LLMs) demonstrate remarkable emergent abilities across various tasks, yet fall short of complex reasoning and planning tasks.
This paper introduces SeeD, a novel and efficient inference framework to optimize runtime speed and GPU memory management concurrently.
arXiv Detail & Related papers (2024-06-26T09:33:41Z) - Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
We present Parsimonious-OPtimal (POP) DPOR algorithm for analyzing multi-threaded programs under sequential consistency.
POP combines several novel techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, and (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions.
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) - Continuous-time convolutions model of event sequences [53.36665135225617]
Huge samples of event sequences data occur in various domains, including e-commerce, healthcare, and finance.
The amount of available data and the length of event sequences per client are typically large, thus it requires long-term modelling.
We propose the COTIC method based on a continuous convolution neural network suitable for non-uniform occurrence of events in time.
arXiv Detail & Related papers (2023-02-13T10:34:51Z) - 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) - ProcessTransformer: Predictive Business Process Monitoring with
Transformer Network [0.06445605125467573]
We propose ProcessTransformer, an approach for learning high-level representations from event logs with an attention-based network.
Our model incorporates long-range memory and relies on a self-attention mechanism to establish dependencies between a multitude of event sequences and corresponding outputs.
arXiv Detail & Related papers (2021-04-01T18:58:46Z) - 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.