論文の概要: Ownership in low-level intermediate representation

• arxiv url: http://arxiv.org/abs/2408.04043v3
• Date: Tue, 13 Aug 2024 13:31:34 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-14 19:58:40.280510
• Title: Ownership in low-level intermediate representation
• Title（参考訳）: 低レベル中間表現におけるオーナシップ
• Authors: Siddharth Priya, Arie Gurfinkel,
• Abstract要約: 高レベルの言語におけるオーナシップの概念は、プログラマとコンパイラの両方がメモリ操作の有効性を判断するのに役立ちます。 低レベル中間表現のようなLLVMのオーナシップセマンティクスを開発する。 LLVMのモデルチェッカーであるSEABMCでこれらのセマンティクスを実装している。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. Previously, ownership semantics has been used successfully in high level automatic program verification to model a reference to data by a first order logic (FOL) representation of data instead of maintaining an address map. However, ownership semantics is not used in low level program verification. We have identified two challenges. First, ownership information is lost when a program is compiled to a low level intermediate representation (e.g., in LLVM IR). Second, pointers in low level programs point to bytes using an address map (e.g., in unsafe Rust) and thus the verification condition (VC) cannot always replace a pointer by its FOL abstraction. To remedy the situation, we develop ownership semantics for an LLVM like low level intermediate representation. Using these semantics, the VC can opportunistically model some memory accesses by a direct access of a pointer cache that stores byte representation of data. This scheme reduces instances where an address map must be maintained, especially for mostly safe programs that follow ownership semantics. For unsafe functionality, memory accesses are modelled by operations on an address map and we provide mechanisms to keep the address map and pointer cache in sync. We implement these semantics in SEABMC, a bit precise bounded model checker for LLVM. For evaluation, the source programs are assumed to be written in C. Since C does not have ownership built in, suitable macros are added that introduce and preserve ownership during translation to LLVM like IR for verification. This approach is evaluated on mature open source C code. For both handcrafted benchmarks and practical programs, we observe a speedup of $1.3x-5x$ during SMT solving.
• Abstract（参考訳）: 高レベルの言語におけるオーナシップの概念は、プログラマとコンパイラの両方がメモリ操作の有効性を判断するのに役立ちます。 これまで、オーナシップセマンティクスは、アドレスマップを維持する代わりに、データの1次論理(FOL)表現によってデータへの参照をモデル化するために、ハイレベルな自動プログラム検証でうまく使われてきた。 しかし、オーナシップのセマンティクスは低レベルのプログラム検証には使われない。 我々は2つの課題を特定した。 まず、プログラムが低レベル中間表現(例えばLLVM IR)にコンパイルされると、所有権情報が失われる。 第二に、低レベルのプログラムのポインタはアドレスマップ(例えば、安全でないRust)を使用してバイトを指しているため、検証条件(VC)は、常にFOL抽象化によってポインタを置き換えることはできない。 状況を改善するため,低レベル中間表現のようなLLVMのオーナシップセマンティクスを開発する。 これらのセマンティクスを使用することで、VCはデータのバイト表現を格納するポインタキャッシュの直接アクセスによって、いくつかのメモリアクセスを同時にモデル化することができる。 このスキームは、特にオーナシップのセマンティクスに従う安全なプログラムに対して、アドレスマップをメンテナンスしなければならないインスタンスを減らす。 安全でない機能のために、メモリアクセスはアドレスマップの操作によってモデル化され、アドレスマップとポインタキャッシュを同期に保つメカニズムを提供する。 LLVMのモデルチェッカーであるSEABMCでこれらのセマンティクスを実装している。 Cにはオーナシップが組み込まれていないため、検証のためにIRのようなLLVMへの変換中にオーナシップを導入して保存する適切なマクロが追加される。 このアプローチは成熟したオープンソースCコードで評価される。 手作りのベンチマークと実用的なプログラムの両方に対して、SMT解決時に13x-5x$のスピードアップを観察する。

関連論文リスト

• FUSELOC: Fusing Global and Local Descriptors to Disambiguate 2D-3D Matching in Visual Localization [57.59857784298536]
  直接2D-3Dマッチングアルゴリズムでは、メモリが大幅に削減されるが、より大きくあいまいな検索空間のために精度が低下する。 本研究では,2次元3次元探索フレームワーク内の重み付き平均演算子を用いて局所的およびグローバルな記述子を融合させることにより,この曖昧さに対処する。 ローカルのみのシステムの精度を常に改善し、メモリ要求を半減させながら階層的な手法に近い性能を達成する。
  論文  参考訳（メタデータ） (2024-08-21T23:42:16Z)
• Host-Based Allocators for Device Memory [1.2289361708127877]
  割り当てアルゴリズムはホストメモリ上で実行されるが、デバイスメモリを割り当てるので、アロケータはアロケータが割り当てているメモリを読み取ることができない。 これはつまり,ほぼすべてのアロケーションアルゴリズムにおいて,ユビキタスな概念である境界タグを使用できない,ということです。 本稿では,この制約を回避するための代替アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2024-05-11T19:28:37Z)
• Enabling Memory Safety of C Programs using LLMs [5.297072277460838]
  C言語で書かれた低レベルのコードのメモリ安全性違反は、ソフトウェア脆弱性の主要な原因のひとつであり続けています。 このような違反を建設によって除去する方法の1つは、安全なC方言にCコードを移植することである。 このような方言は、最小限のランタイムオーバーヘッドで安全性を保証するためにプログラマが提供するアノテーションに依存している。 この移植は、プログラマに多大な負担をかける手作業であり、そのため、このテクニックの採用は限られている。
  論文  参考訳（メタデータ） (2024-04-01T13:05:54Z)
• SeMalloc: Semantics-Informed Memory Allocator [18.04397502953383]
  UAF(Use-after-free)は、メモリアンセーフ言語において重要な問題である。 ヒープオブジェクトに関するより多くのセマンティクスをアロケータに渡すことで、トリニティをバランスさせる方法の1つを示します。 SeMallocでは、同じコールサイトから割り当てられたヒープオブジェクトと、同じ関数呼び出しスタックを介して、仮想メモリアドレスを共有することができる。
  論文  参考訳（メタデータ） (2024-02-02T21:02:15Z)
• A Semantic Space is Worth 256 Language Descriptions: Make Stronger Segmentation Models with Descriptive Properties [53.177550970052174]
  ProLabは、プロパティレベルのラベル空間を使用して、強力な解釈可能なセグメンテーションモデルを作成する新しいアプローチである。 セグメンテーションモデルを監督するために、常識知識に根ざした記述的特性を使用する。
  論文  参考訳（メタデータ） (2023-12-21T11:43:41Z)
• CRIL: A Concurrent Reversible Intermediate Language [0.0]
  本稿では,高レベル並列言語を他の低レベル並列言語に翻訳するための構成の可逆中間言語を提案し,可逆性を維持する。 機能的可逆言語としてMogensen が用いた RIL の拡張として CRIL を提案し,P-V 演算に基づくマルチスレッドプロセス呼び出しと同期プリミティブを組み込んだ。
  論文  参考訳（メタデータ） (2023-09-13T20:52:54Z)
• rCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust [4.616001680122352]
  Rustはコンパイル時の検証を通じてメモリ安全性を保証するシステムプログラミング言語である。 本稿では,半自動境界を越えたリークを検出する静的,非自動,完全自動モデルチェッカーであるrCanaryを提案する。
  論文  参考訳（メタデータ） (2023-08-09T08:26:04Z)
• Side Adapter Network for Open-Vocabulary Semantic Segmentation [69.18441687386733]
  本稿では,Side Adapter Network (SAN) という,事前学習された視覚言語モデルを用いたオープン語彙セマンティックセマンティックセマンティックセマンティクスのための新しいフレームワークを提案する。 サイドネットワークは凍結したCLIPモデルにアタッチされ、ひとつはマスクの提案を予測し、もうひとつは注意バイアスを予測する。 トレーニング可能なパラメータは最大で18倍,推論速度は19倍に向上した。
  論文  参考訳（メタデータ） (2023-02-23T18:58:28Z)
• Learning Implicit Feature Alignment Function for Semantic Segmentation [51.36809814890326]
  Implicit Feature Alignment Function (IFA)は、暗黙の神経表現の急速に拡大するトピックにインスパイアされている。 IFAは機能マップを異なるレベルで暗黙的に整列し、任意の解像度でセグメンテーションマップを生成することができることを示す。 提案手法は,様々なアーキテクチャの改善と組み合わせて,一般的なベンチマークにおける最先端の精度のトレードオフを実現する。
  論文  参考訳（メタデータ） (2022-06-17T09:40:14Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  ソースコードにnlpプリトレーニング技術を直接適用するか、あるいはtheshelfによってモデルに機能を追加するかで、プログラムをより理解するためのモデルを構築するのは難しい。 本研究では,(1)操作セマンティクスの基本操作とよく一致する表現と(2)環境遷移の情報からなる情報から,モデルが学ぶべき新しいプログラムセマンティクス学習パラダイムを提案する。
  論文  参考訳（メタデータ） (2021-05-10T12:21:42Z)
• Kanerva++: extending The Kanerva Machine with differentiable, locally block allocated latent memory [75.65949969000596]
  エピソディックメモリとセマンティックメモリは、人間のメモリモデルの重要なコンポーネントです。 我々は、エピソードメモリとセマンティックメモリのギャップを埋める新しい原理ベイズメモリ割り当てスキームを開発しました。 この割り当て方式がメモリ条件画像生成の性能を向上させることを実証する。
  論文  参考訳（メタデータ） (2021-02-20T18:40:40Z)

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

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