論文の概要: 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アルゴリズムよりも指数関数的に高速であり, 不要な実行探索を完全に回避できることを示した。

関連論文リスト

• Grounding Partially-Defined Events in Multimodal Data [61.0063273919745]
  部分定義イベントに対するマルチモーダル定式化を導入し、これらのイベントの抽出を3段階スパン検索タスクとしてキャストする。 このタスクのベンチマークであるMultiVENT-Gを提案し,22.8Kのラベル付きイベント中心エンティティを含む,14.5時間の高密度アノテーション付き現在のイベントビデオと1,168のテキストドキュメントからなる。 結果は、イベント理解の抽象的な課題を示し、イベント中心のビデオ言語システムにおける約束を実証する。
  論文  参考訳（メタデータ） (2024-10-07T17:59:48Z)
• A Learning Support Method for Multi-threaded Programs Using Trace Tables [0.0]
  マルチスレッドプログラムは、並列処理のためにアプリケーションプロセスを複数のスレッドに分割することで、応答性とリソースの保存を改善することが期待されている。 しかし、スケジューリングと複数のスレッドの相互作用のため、実行時の動作はシングルスレッドプログラムよりも複雑である。 トレーステーブルを用いたマルチスレッドプログラムの学習ツールを提案する。
  論文  参考訳（メタデータ） (2024-09-25T07:46:38Z)
• Event-ECC: Asynchronous Tracking of Events with Continuous Optimization [1.9446776999250501]
  イベントECC (eECC) という,イベントごとの2次元運動ワープを計算するトラッキングアルゴリズムを提案する。 イベント処理の計算負担は、インクリメンタル処理と更新スキームの恩恵を受ける軽量バージョンによって軽減される。 最先端のイベントベース非同期トラッカーにおける追跡精度と特徴年齢の改善について報告する。
  論文  参考訳（メタデータ） (2024-09-22T19:03:19Z)
• Parsimonious Optimal Dynamic Partial Order Reduction [1.5029560229270196]
  本稿では,Parsimonious-Optimal DPOR(POP)を提案する。 POPは、(i)同じ人種の複数の逆転を避ける擬似的な人種反転戦略を含む、いくつかの新しいアルゴリズム技術を組み合わせている。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。
  論文  参考訳（メタデータ） (2024-05-18T00:07:26Z)
• Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
  Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。 まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。 我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
  論文  参考訳（メタデータ） (2023-05-22T06:11:15Z)
• 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)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。