文献

J-GLOBAL ID：202202228217998831   整理番号：22A1053015

持続性x86-TSOのためのビューベースOwicki-Gries推論【JST・京大機械翻訳】

View-Based Owicki-Gries Reasoning for Persistent x86-TSO

著者 (5件)： Bila Eleni Vafeiadi (University of Surrey, Guildford, UK) ,  Dongol Brijesh (University of Surrey, Guildford, UK) ,  Lahav Ori (Tel Aviv University, Tel Aviv, Israel) ,  Raad Azalea (Imperial College London, London, UK) ,  Wickerson John (Imperial College London, London, UK)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13240  ページ： 234-261  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 持続的メモリの上昇は,そのコアへのコンピューティングを混乱させる。本研究は,メモリアクセスやフェンスのような低レベル操作,ならびにフラッシュのような持続性プリミティブを用いる,x86コードに関する推論のためのプログラム論理を提供することにより,プログラマがこの br新世界をナビゲートするのを助けることを目的とする。この論理,Pierogiは,ビューに基づく単純な基礎となる操作意味論から利益を得て,最適化フラッシュ操作を処理でき,Isabelle/HOL証明支援で機械化される。Pierogiの証明規則を詳述し,それらの音を証明した。また,Pierogiが,一連の挑戦的な単一およびマルチスレッドの持続的プログラムを理由としてどのように使用できるかも示した。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 記憶装置 ,  最適化 ,  機械化 ,  プログラマ ,  論理 ,  音響 ,  規則 ,  *推論 ,  検証 ,  操作的意味論 ,  マルチスレッド
準シソーラス用語： 塀 ,  メモリアクセス , 【Automatic Indexing@JST】

著者キーワード (5件)： 持続的記憶 ,  x86-TSO ,  Owicki-Gries ,  Isabelle/HOL ,  検証

分類 (4件)： 計算機システム開発  (JD02010R) ,  汎用プログラミング言語  (JD03051H) ,  言語プロセッサ  (JD03040F) ,  記憶方式  (JC02040V)

タイトルに関連する用語 (2件)： 持続性 ,  推論