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

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

Group

PRINCIPIA

Number of events 96

Members 244

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 メモリモデルの分析 に参加を申し込みました!

bluee

bluee

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)