お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
2024年5月23日(木)以降より開始予定の「connpass 有料API」の料金プランにつきましてはこちらをご覧ください。

お知らせ connpassをご利用いただく全ユーザーにおいて健全で円滑なイベントの開催や参加いただけるよう、イベント参加者向け・イベント管理者向けのガイドラインページを公開しました。内容をご理解の上、イベント内での違反行為に対応する参考としていただきますようお願いいたします。

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

Sep

1

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

Organizing : PRINCIPIA Limited

x86-TSO メモリモデルの分析
Hashtag :#形式手法
Registration info

一般

Free

FCFS
29/30

Attendees
kahirokunn
niszet
bluee
tanimocchi
TakeshiHori
matsud224
Ken Sonoda
rjkuro
yak_ex
keisukefukuda
View Attendee List
Start Date
2020/09/01(Tue) 20:30 ~ 21:30
Registration Period

2020/08/24(Mon) 00:00 〜
2020/09/01(Tue) 20:00まで

Location

Zoom

オンライン

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

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)