枯れた技術の水平思考

世の中わからないことだらけだ.少し確かなことは検証をしたことだけ

「Goで作って理解するRaftベースRedis互換KVS」に関する情報ページ

販売サイト

techbookfest.org

リポジトリ

v1.0 における正誤表

記述の誤り

p.21

Quiescent ConsistencyとLinearizabilityの違いを明確化

誤:

また、操作の実行順序と実時間の順序が一致することが重要です。これにより、システムの挙動が予測しやすくなる一方で、実装の複雑さやパフォーマンスへの影響が大きくなることがあります。

正:

また、ある操作が別の操作より前に完了した場合、その操作は必ず前の操作の後に見えなければなりません。これにより、システムの挙動が予測しやすくなる一方で、実装の複雑さやパフォーマンスへの影響が大きくなることがあります。

p. 23

誤:

 ただし、ユーザーによっては操作が異なる順序で見える場合があります。

正:

 (削除)

kumagiさんによる解説:

逐次一貫性までは全部強整合性アルゴリズムもしくはサーバサイド一貫性の仲間なのでユーザーによって観測順序が変わる事はない。

p. 32

誤:

形式手法は、数学的な証明を用いて、システムの仕様を記述し、その仕様が満たされていることを証明する手法です。

形式手法は、システムの設計や検証に数学的および論理的な方法を用いる技術です。これにより、システムの正確性や一貫性を厳密に検証し、バグや誤動作を未然に防ぐことができます。特に、安全性や信頼性が求められる領域で重要視されています。

例えば、AWSでは、S3やDynamoDB、EBSなどのサービスにおいて、形式手法を用いた安全性の確認を行っています。
出典: [Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff: Use of Formal Methods at Amazon Web Services](https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf) 

p. 33

単一障害点という表現がRaftの文脈で適切ではないため、より正しい表現に修正する。

誤:

リーダーが単一障害点となり、新しいリーダー選出までの間、システムの可用性が低下する

正:

リーダー障害時には、新しいリーダー選出までの間、システムの可用性が一時的に低下する。

kumagiさんによる解説:

Raftの語彙の中ではSPoFとは呼ばないのではないかなこれ。failure detectorは語りだすと長いんだけどcrash recover上ではダウンタイムを完全にゼロにするのは理論的に無理な気がする(flp impossibilityと似た感じで

表記の誤り

p. 62

誤:

著者が公開している ?? というものがあり

正:

著者が公開している [https://github.com/bootjp/elastickv] というものがあり

p.64

誤:

Timestamp Oraclee 

正:

Timestamp Oracle 

v1.1における正誤表

記述の誤り

p29

誤:

コミットインデックスはクライアントに返答が行われる前に、クラスタ内の過半数の
ノードに適用されたログエントリのインデックスを示します。
コミットインデックスは、クラスタ内の過半数のノードに保存され、リーダーがコミットした最新のログエントリのインデックスを示します。