新機能 イベントメッセージの予約機能を追加しました。イベント主催者様は、参加者へのメッセージ送信を事前に予約できます。詳しくはこちらをご確認ください。

新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

このエントリーをはてなブックマークに追加

Sep

1

x86-TSO メモリモデルの分析

Organizing : PRINCIPIA Limited

Hashtag :#形式手法
Registration info

一般

Free

FCFS
29/30

Description

x86-TSO メモリモデルの分析

x86 CPU のメモリモデルは Intel および AMD のマニュアルにおいて自然言語によって記述されていますが,記述が曖昧であったり実際の CPU の挙動とは異なるものがあったりしたそうです.

文献 [1] ではマニュアルの複数の版を調査し,さらに実 CPU についても調査した結果を踏まえて,形式的な x86 のメモリモデルを構築しています.

このメモリモデル x86-TSO をプロセス代数 CSP で記述し,CSP に基づく詳細化検査器(refinement checker)SyncStitch で分析してみたので軽く紹介したいと思います.

一度形式モデルができると様々なケースを調べることができます.実用的な例として,文献 [2] で紹介されている Linux kernel の実装で議論になった spin lock 実装の安全性を検査してみます.

Zoom を使用します.meeting の URL はイベント申し込み締め切り時刻後に CONNPASS のメッセージにてお知らせします.

参考文献

[1] A Better x86 Memory Model: x86-TSO,Scott Owens, Susmit Sarkar, Peter Sewell, 2009

[2] x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors, Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa nardelli, and Magnus O. Myreen, 2010

Media View all Media

If you add event media, up to 3 items will be shown here.

Feed

hatsugai

hatsugai published x86-TSO メモリモデルの分析.

08/24/2020 08:58

Ended

2020/09/01(Tue)

20:30
21:30

Registration Period
2020/08/24(Mon) 00:00 〜
2020/09/01(Tue) 20:00

Location

Zoom

オンライン

Zoom

Organizer

Attendees(29)

kahirokunn

kahirokunn

x86-TSO メモリモデルの分析に参加を申し込みました!

niszet

niszet

x86-TSO メモリモデルの分析 に参加を申し込みました!

blue271828

blue271828

x86-TSO メモリモデルの分析に参加を申し込みました!

tanimocchi

tanimocchi

x86-TSO メモリモデルの分析 に参加を申し込みました!

TakeshiHori

TakeshiHori

x86-TSO メモリモデルの分析 に参加を申し込みました!

matsud224

matsud224

x86-TSO メモリモデルの分析に参加を申し込みました!

Ken Sonoda

Ken Sonoda

x86-TSO メモリモデルの分析に参加を申し込みました!

rjkuro

rjkuro

I joined x86-TSO メモリモデルの分析!

yak_ex

yak_ex

x86-TSO メモリモデルの分析 に参加を申し込みました!

keisukefukuda

keisukefukuda

x86-TSO メモリモデルの分析 に参加を申し込みました!

Attendees (29)

Canceled (1)