論文の概要: Towards Bug-Free Distributed Go Programs
- arxiv url: http://arxiv.org/abs/2506.15135v2
- Date: Fri, 25 Jul 2025 06:48:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-28 14:14:27.237382
- 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プログラミング言語のサブセットを用いた分散プログラムにおける通信競合の欠如を証明するための検証フレームワークについて述べる。
我々は、分散プログラムがどのように実行されるのかを静的に推論し、フェール・バイ・オーダを使用してバッファリングおよび未バッファリングのチャネルに拡張する。
関連論文リスト
- Secure Quantum Relay Networks Using Distributed Entanglement without Classical Authentication [0.0]
現在の量子通信プロトコルは、メッセージ元検証の古典的な認証に大きく依存している。
古典的認証を完全に回避するセキュアな量子中継ネットワークのための新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2025-07-07T20:25:10Z) - 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) - Generative AI-aided Joint Training-free Secure Semantic Communications
via Multi-modal Prompts [89.04751776308656]
本稿では,多モデルプロンプトを用いたGAI支援型SemComシステムを提案する。
セキュリティ上の懸念に応えて、フレンドリーなジャマーによって支援される隠蔽通信の応用を紹介する。
論文 参考訳(メタデータ) (2023-09-05T23:24:56Z) - 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) - Semantic Communications: Principles and Challenges [59.13318519076149]
本稿では,セマンティックコミュニケーションの概要を紹介する。
シャノン情報理論の簡単なレビューの後、深層学習によって実現される理論、フレームワーク、システム設計とのセマンティックコミュニケーションについて論じる。
論文 参考訳(メタデータ) (2021-12-30T16:32:00Z) - Mutually Unbiased Balanced Functions & Generalized Random Access Codes [0.0]
ランダムアクセスコード(RAC)は、暗号的に重要な双方向通信タスクのファミリーである。
本稿では,受信者がランダムに選択した入力文字列の関数を検索することを目的とした,このタスクの一般化を提案する。
我々は、古典的(II)量子準備と測度、および(iii)エンタングルメント支援古典的通信(EACC)プロトコルの性能を、結果の一般化RAC(GRAC)に対して検討し、バウンドする。
論文 参考訳(メタデータ) (2021-05-09T13:17:24Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。