論文の概要: Towards Bug-Free Distributed Go Programs

• arxiv url: http://arxiv.org/abs/2506.15135v1
• Date: Mon, 16 Jun 2025 17:19:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-19 19:35:51.549995
• Title: Towards Bug-Free Distributed Go Programs
• Title（参考訳）: バグフリーの分散Goプログラムを目指して
• Authors: Zhengqun Koo,
• Abstract要約: 本稿では,分散プログラムにおける通信競合の欠如を証明できる検証フレームワークについて述べる。 我々は、分散プログラムがどのように実行されるのかを静的に推論し、フェール・バイ・オーダを使用してバッファリングおよび未バッファリングのチャネルに拡張する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Programmers of distributed systems need to reason about concurrency to avoid races. However, reasoning about concurrency is difficult, and unexpected races show up as bugs. Data race detection in shared memory systems is well-studied (dynamic data race detection [13], behavioral types [15], dynamic race detection [31]). Similar to how a data race consists of reads and writes not related by happens-before at a shared memory location, a communication race consists of receives and sends not related by happens-before on a shared channel. Communication races are problematic: a receiver expects a specific message from a specific sender, but with a communication race, the receiver can receive a message meant for another receiver, or not receive anything at all. In this work, we describe a verification framework that can prove the absence of communication races for distributed programs that use a subset of the Go programming language, where synchronization is mainly achieved via message passing. We statically reason about how a distributed program executes, using a happens-before order, extended to buffered and unbuffered channels.
• Abstract（参考訳）: 分散システムのプログラマは、競合を避けるために並行性について考える必要があります。 しかしながら、並行性に関する推論は難しく、予期せぬレースがバグとして現れます。 共有メモリシステムにおけるデータ競合検出は、よく研究されている(動的データ競合検出[13]、行動型[15]、動的競合検出[31])。 データレースは、共有メモリロケーションで発生前と関係のない読み取りと書き込みで構成されているのと同じように、通信レースは受信から成り、共有チャネルで発生前と関係のない送信から成り立っている。 受信側は特定の送信側からの特定のメッセージを期待するが、通信側は受信側が他の受信側に対してメッセージを受け取るか、受信側が何も受信しないかのどちらかである。 本稿では,Goプログラミング言語のサブセットを用いた分散プログラムにおける通信競合の欠如を証明するための検証フレームワークについて述べる。 我々は、分散プログラムがどのように実行されるのかを静的に推論し、フェール・バイ・オーダを使用してバッファリングおよび未バッファリングのチャネルに拡張する。

関連論文リスト

• A Compressive-Expressive Communication Framework for Compositional Representations [0.6937243101289334]
  本稿では,事前学習モデルから学習した表現の合成性を誘導する自己教師型フレームワークCELEBIを紹介する。 提案手法は,Shapes3DおよびMPI3Dデータセット上での学習メッセージの効率性と構成性を向上する。 この研究は、単純性に基づく帰納的バイアスから構造化された一般化可能な通信プロトコルが出現する新たな理論的および実証的な証拠を提供する。
  論文  参考訳（メタデータ） (2025-01-31T14:46:11Z)
• Optimistic Prediction of Synchronization-Reversal Data Races [6.407713444542916]
  動的データ競合検出は、実際に並列ソフトウェアの信頼性を確保するための重要なテクニックとして登場した。 本研究では,抽出可能な方法で検出可能なOptimistic Sync(hronization)-Reversal racesと呼ばれるデータレースのクラスを同定する。 また、全2次時間における全楽観的同期反転データ競合を検出するための音響アルゴリズムOSRを提案する。
  論文  参考訳（メタデータ） (2024-01-11T03:34:21Z)
• Cognitive Semantic Communication Systems Driven by Knowledge Graph: Principle, Implementation, and Performance Evaluation [74.38561925376996]
  単一ユーザと複数ユーザのコミュニケーションシナリオに対して,認知意味コミュニケーションフレームワークが2つ提案されている。 知識グラフから推論規則をマイニングすることにより,効果的な意味補正アルゴリズムを提案する。 マルチユーザ認知型セマンティックコミュニケーションシステムにおいて,異なるユーザのメッセージを識別するために,メッセージ復元アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-03-15T12:01:43Z)
• Semantic-Native Communication: A Simplicial Complex Perspective [50.099494681671224]
  トポロジカル空間の観点から意味コミュニケーションを研究する。 送信機はまずデータを$k$の単純複素数にマッピングし、その高次相関を学習する。 受信機は構造を復号し、行方不明または歪んだデータを推測する。
  論文  参考訳（メタデータ） (2022-10-30T22:33:44Z)
• Neuro-Symbolic Causal Reasoning Meets Signaling Game for Emergent Semantic Communications [71.63189900803623]
  創発的SCシステムフレームワークを提案し,創発的言語設計のためのシグナリングゲームと因果推論のためのニューロシンボリック(NeSy)人工知能(AI)アプローチで構成されている。 ESCシステムは、意味情報、信頼性、歪み、類似性の新たな指標を強化するように設計されている。
  論文  参考訳（メタデータ） (2022-10-21T15:33:37Z)
• Unifying Event Detection and Captioning as Sequence Generation via Pre-Training [53.613265415703815]
  本稿では,イベント検出とキャプションのタスク間関連性を高めるための,事前学習と微調整の統合フレームワークを提案する。 我々のモデルは最先端の手法よりも優れており、大規模ビデオテキストデータによる事前学習ではさらに向上できる。
  論文  参考訳（メタデータ） (2022-07-18T14:18:13Z)
• Inferring Unobserved Events in Systems With Shared Resources and Queues [0.8602553195689513]
  実生活システムは、しばしば起こる全ての出来事のサブセットのみを記録する。 共有リソースを持つプロセスの動作を理解し,分析するために,発生したに違いないが記録されていないイベントのタイムスタンプの境界を再構築することを目的としている。 我々は、非観測イベントのタイムスタンプを効率的に導き出すために、エンティティトレース上の線形プログラミングを使用する。
  論文  参考訳（メタデータ） (2021-02-27T09:34:01Z)
• Undoing Causal Effects of a Causal Broadcast Channel with Cooperating Receivers using Entanglement Resources [0.0]
  我々は、変調和に依存する因果的放送チャンネル上での通信シナリオを解析する。 受信機が絡み合いを共有し、古典的な通信を行うことができれば、メッセージはゼロではない速度で、検証可能な安全なコラボレーションで受信できることがわかった。
  論文  参考訳（メタデータ） (2021-02-15T10:05:04Z)

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

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