ロックフリーアルゴリズムとは，正確には進行性が保証されるアルゴリズムのことをいう．Compare and Swap命令(CAS)を主軸として実装する．
ロックフリーアルゴリズムにおいて，有名な問題としてABA問題がある．ABA問題の解決方法はいくつかあり，それぞれに特徴がある．今回は，タグ付きポインタとload-link/store-conditional(ll/sc)バージョンでのCASといった2つの解決方法について検証する．
最初に，ロックフリーアルゴリズムのなかで最も基本的なロックフリースタックをC言語で実装する．そして，それをPromelaでSPINのモデルとして記述する．
| // The template for writing concurrent program to experiment | |
| #include <atomic> | |
| #include <cstdio> | |
| #include <thread> | |
| #include <vector> | |
| const static unsigned int producer = 1; | |
| const static unsigned int consumer = 2; | |
| static std::atomic<int> val(0); |
| #ifndef _GNU_SOURCE | |
| #define _GNU_SOURCE | |
| #endif | |
| #include <atomic> | |
| #include <cstdio> | |
| #include <linux/futex.h> | |
| #include <sys/syscall.h> | |
| #include <sys/types.h> | |
| #include <thread> | |
| #include <unistd.h> |
| # 参考文献 | |
| ## 事例系 | |
| [By Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser | |
| Communications of the ACM, October 2018, Vol. 61 No. 10, Pages 68-77 | |
| Formally Verified Software in the Real World | |
| ### 要約 | |
| ボーイング社の軍用ヘリでの事例。seL4ベースにどうシステムをセキュリティを担保したかという話。重要なこととして、 |