文献

J-GLOBAL ID：202002279895977860   整理番号：20A2638438

認証と効率的な命令スケジューリング:インターロックVLIWプロセッサへの応用【JST・京大機械翻訳】

Certified and efficient instruction scheduling: application to interlocked VLIW processors

著者 (3件)： Six Cyril (Kalray, France / Grenoble Alps University, France / CNRS, France / Grenoble INP, France / VERIMAG, France) ,  Boulme Sylvain (Grenoble Alps University, France / CNRS, France / Grenoble INP, France / VERIMAG, France) ,  Monniaux David (Grenoble Alps University, France / CNRS, France / Grenoble INP, France / VERIMAG, France)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 4  号： OOPSLA  ページ： 1-29  発行年： 2020年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： Compertは,正式,機械検査,正しさの証明を有する適度に最適化するCコンパイラであり,成功した編集の後,組立コードはソースコードに忠実な挙動を持っている。以前に,それは逐次意味論を有する目標命令セットだけをサポートして,最適化のための指示命令を試みなかった。ここでは,VLIWコア(即ち,命令レベルで明示的並列性を持つ)に対するCompCertバックエンド,スケーラブルで効率的な命令スケジューリングを提供する最初のCompCertバックエンドを提示した。さらに,その高度モジュール実装は,他のVLIWまたは非VLIWパイプラインプロセッサに容易に適応できる。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 最適化 ,  意味論 ,  コンパイラ ,  機械的検査 ,  *演算プロセッサ ,  命令セット
準シソーラス用語： *VLIWアーキテクチャ ,  バックエンド ,  形式的検証 ,  ILP【並列性】 ,  ソースコード ,  *命令スケジューリング , 【Automatic Indexing@JST】

著者キーワード (5件)： コンパイラ最適化の形式的検証 ,  ハッシュコンシング ,  命令レベル並列性 ,  記号実行 ,  Coq証明アシスタント

分類 (2件)： 言語プロセッサ  (JD03040F) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (6件)： 認証 ,  命令スケジューリング ,  ロック ,  VLIW ,  プロセッサ ,  応用