論文の概要: Tailoring Stateless Model Checking for Event-Driven Multi-Threaded
Programs
- arxiv url: http://arxiv.org/abs/2307.15930v1
- Date: Sat, 29 Jul 2023 08:43:49 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-23 16:02:42.158709
- Title: Tailoring Stateless Model Checking for Event-Driven Multi-Threaded
Programs
- Title(参考訳): イベント駆動マルチスレッドプログラムのためのステートレスモデルチェックの調整
- Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer B{\o}nneland,
Sarbojit Das, Bengt Jonsson, Magnus L{\aa}ng, and Konstantinos Sagonas
- Abstract要約: イベント駆動型プログラムに適したDPORアルゴリズムであるEvent-DPORを提案する。
これはマルチスレッドプログラムのための最適DPORアルゴリズムであるOptimal-DPORに基づいている。
全てのプログラムに対して Event-DPOR の正当性を証明し,大規模サブクラスに対して最適性を示す。
- 参考スコア(独自算出の注目度): 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.
- Abstract(参考訳): イベント駆動型マルチスレッドプログラミングは並列計算を構築する上で重要なイディオムである。
Stateless Model Checking (SMC) は、特に動的部分順序減少(DPOR)と組み合わせた場合、マルチスレッドプログラムの有効な検証手法である。
既存のSMC技術は、イベントが競合しない場合でも、イベント処理の可能な全ての順序を探索するので、イベント駆動プログラムを扱うのに効果がないことが多い。
イベント駆動型マルチスレッドプログラムに適したDPORアルゴリズムであるEvent-DPORを提案する。
マルチスレッドプログラムのための最適DPORアルゴリズムであるOptimal-DPORに基づいており、イベント駆動プログラムにどのように拡張できるかを示す。
全てのプログラムのイベントdporの正しさと、大きなサブクラスの最適性を証明する。
複雑化の1つは、新しい実行の冗長性をチェックするevent-dporの操作がnp-hardであることである。
実装と実験により, ハンドラスレッドをロックを用いてシミュレートする他のツールと比較して, Event-DPORは, 各種プログラムにおける他の最先端DPORアルゴリズムよりも指数関数的に高速であり, 不要な実行探索を完全に回避できることを示した。
関連論文リスト
- Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳(メタデータ) (2023-05-22T06:11:15Z) - Continuous-time convolutions model of event sequences [53.36665135225617]
イベントシーケンスデータの巨大なサンプルは、eコマース、ヘルスケア、ファイナンスなど、さまざまなドメインで発生します。
利用可能なデータの量とクライアント毎のイベントシーケンスの長さは典型的には大きいため、長期的なモデリングが必要である。
時間内の事象の一様発生に適した連続畳み込みニューラルネットワークに基づくCOTIC法を提案する。
論文 参考訳(メタデータ) (2023-02-13T10:34:51Z) - Unifying Event Detection and Captioning as Sequence Generation via
Pre-Training [53.613265415703815]
本稿では,イベント検出とキャプションのタスク間関連性を高めるための,事前学習と微調整の統合フレームワークを提案する。
我々のモデルは最先端の手法よりも優れており、大規模ビデオテキストデータによる事前学習ではさらに向上できる。
論文 参考訳(メタデータ) (2022-07-18T14:18:13Z) - Modeling Continuous Time Sequences with Intermittent Observations using
Marked Temporal Point Processes [25.074394338483575]
人間の活動を通じて生成された大量のデータは、連続した時間のイベントのシーケンスとして表現することができる。
これらの連続的なイベントシーケンスに対するディープラーニングモデルは、非自明なタスクである。
本研究では,イベントシーケンスが欠落している場合にMTPPを学習するための新しい教師なしモデルと推論手法を提案する。
論文 参考訳(メタデータ) (2022-06-23T18:23:20Z) - What Averages Do Not Tell -- Predicting Real Life Processes with
Sequential Deep Learning [0.1376408511310322]
プロセスマイニング(Process Mining)は、システムによってログされた実行データからビジネスプロセスに関する洞察を発見すること。
多くのディープラーニング技術が、プロセス結果の予測を目的とした予測プロセスマイニングに成功している。
プロセスマイニングのトレースはマルチモーダルシーケンスであり、自然言語の文や画像とは全く異なる構造である。
論文 参考訳(メタデータ) (2021-10-19T19:45:05Z) - ProcessTransformer: Predictive Business Process Monitoring with
Transformer Network [0.06445605125467573]
本稿では,イベントログから高レベル表現を注目ネットワークで学習するプロセストランスフォーマーを提案する。
本モデルでは,複数イベントシーケンスと対応する出力の依存関係を確立するための自己保持機構を,長期記憶に取り入れた。
論文 参考訳(メタデータ) (2021-04-01T18:58:46Z) - Inferring Unobserved Events in Systems With Shared Resources and Queues [0.8602553195689513]
実生活システムは、しばしば起こる全ての出来事のサブセットのみを記録する。
共有リソースを持つプロセスの動作を理解し,分析するために,発生したに違いないが記録されていないイベントのタイムスタンプの境界を再構築することを目的としている。
我々は、非観測イベントのタイムスタンプを効率的に導き出すために、エンティティトレース上の線形プログラミングを使用する。
論文 参考訳(メタデータ) (2021-02-27T09:34:01Z) - GRAPHSPY: Fused Program Semantic-Level Embedding via Graph Neural
Networks for Dead Store Detection [4.82596017481926]
低オーバーヘッドで不必要なメモリ操作をインテリジェントに識別するための学習精度の高いアプローチを提案する。
プログラムセマンティクスの抽出にいくつかの有意なグラフニューラルネットワークモデルを適用することにより,新しいハイブリッドなプログラム埋め込み手法を提案する。
その結果、我々のモデルは精度の90%を達成でき、最先端ツールのオーバーヘッドの半分程度しか発生しないことがわかった。
論文 参考訳(メタデータ) (2020-11-18T19:17:15Z) - Process Discovery for Structured Program Synthesis [70.29027202357385]
プロセスマイニングにおける中核的なタスクは、イベントログデータから正確なプロセスモデルを学ぶことを目的としたプロセス発見である。
本稿では,ターゲットプロセスモデルとして(ブロック-)構造化プログラムを直接使用することを提案する。
我々は,このような構造化プログラムプロセスモデルの発見に対して,新たなボトムアップ・アグリメティブ・アプローチを開発する。
論文 参考訳(メタデータ) (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]
本稿では、イベントシーケンス生成のための新規でシンプルなモデルを提案し、ビデオ中のイベントシーケンスの時間的関係を探索する。
提案モデルでは,非効率な2段階提案生成を省略し,双方向時間依存性を条件としたイベント境界を直接生成する。
総合システムは、チャレンジテストセットの9.894 METEORスコアで、ビデオタスクにおける密封イベントの最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2020-06-14T13:21:37Z) - Dynamic Multi-Robot Task Allocation under Uncertainty and Temporal
Constraints [52.58352707495122]
本稿では,不確実性およびマルチエージェント協調の下での逐次意思決定における重要な計算課題を分離するマルチロボット割当アルゴリズムを提案する。
都市におけるマルチアームコンベヤベルトピック・アンド・プレイスとマルチドローン配送ディスパッチの2つの異なる領域における広範囲なシミュレーション結果について検証を行った。
論文 参考訳(メタデータ) (2020-05-27T01:10:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。