タグ検索の該当結果が少ないため、タイトル検索結果を表示しています。
はじめに 分散合意アルゴリズム Raft とは 分散合意アルゴリズムとは Raft の特徴 Raft が満たす性質 Election Safety Leader Append-Only Log Matching Leader Completeness State Machine Safety TLA+ とは TLA+ による Raft の形式的仕様 TLA+ による Raft の検証方法 TLA+ Toolbox のインストール 新規 Spec の作成 Model の作成と実行 補足: コマンドラインでの検証 Raft の拡張について Leadership Transfer Membership Change Log Compaction Client Interaction おわりに Raft 理解度を調べるクイズ 参考資料 Raft に関する資料 TLA+ に関する資料 はじめに この
実践TLA+ | 翔泳社
設計だってテストしたい！ 【本書の内容】 本書は Hillel Wayne, "Practical TLA+", Apress, 2018 の邦訳版です。 複雑精緻なシステムを構築する際に、設計そのもの、仕様そのものにバグがないかをテストできたら、もう少し幸せな開発人生を送れそうな気がします。 本書は送金システムの小規模な仕様からTLA+を使ってヤバいバグを発見するところから始まります。この小さなサンプルをもとに、より良いアプリケーションの設計・テスト・構築に、どのようにTLA+を使えばよいかを理解し、実際のプロジェクトに援用できるよう、TLA+の演算子、論理、関数、PlusCal、モデル、および同時実行の基礎を学びます。 設計図の整理の仕方、分散システムや最終的な整合性の指定の仕方を学んだら、アルゴリズムのパフォーマンスやデータ構造、ビジネスコードやMapReduceなど、さまざまな実用
July Tech Festa 2021 winter で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 インフラ技術のカンファレンス July Tech Festa 2021 winter で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 www.youtube.com 今回の登壇は、昨年の CloudNative Days Tokyo 2020 と同じ題材を扱っています。ただ、前回より持ち時間が長くなった分、前回のスライドで説明不足だった部分を拡充してあります。特に、CockroachDB 以外の TLA+ 採用事例や、分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。 なお、前回の登壇報告は以下の記事をご参照ください。 ccvanishing.hateblo.jp 当日出た質問 実時間を含む性質 今回の時相論理では「いつか成り立つ」と
Using TLA+ in the Real World to Understand a Glibc Bug by Malte Skarupke TLA+ is a formal specification language that you can use to verify programs. It’s different from other formal verification systems in that it’s very pragmatic. Instead of writing proofs, it works using the simple method of running all possible executions of a program. You can write assertions and if they’re not true for any p
【大正解】キーボードはR2TLA-JPV-IVが一番おすすめ！
借金を200万円抱えた状態でアフィリエイターとして独立。そこから月収250万円に。アフィリエイトで人生を逆転した僕の体験談やSEOの方法を書いていきます。
CloudNative Days Tokyo 2020 で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、
Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述（特にTLA+）とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。 ソフトウェアの仕様を形式仕様で厳密に書き下して検証、証明するという手法がある！ということ自体は院生時代に見聞きして知ってたんですが「難しそう」とか「一部のすごい人にしか使えなさそう」といった先入観があってなんとなく敬遠してました。正直、当時は自分の身近な問題であると感じられていませんでした。 あれから10年以上たって最近形式仕様記述とかModel checkingとかTheorem provingというものは「必須なものである」という認識がようやく私の中にも芽生えたようです。仕事で分散システムの開発を通じて「これは人間の頭
My job these days is teaching TLA+ and formal methods: specifying designs to find bugs in them. But just knowing the syntax isn’t enough to write specs, and it helps to have examples to draw from. I recently read Chris Siebenmann’s Even in Go, concurrency is still not easy and thought it would make a good case study for writing a spec. In it, he gives an example of Go code which deadlocks: /*1 */
GitHub - informalsystems/quint: An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
module secret_santa { const participants: Set[str] /// get(recipient_for_santa, S) is the recipient for secret santa S var recipient_for_santa: str -> str /// the bowl of participants, containing a paper piece for each participant name var bowl: Set[str] val santas = recipient_for_santa.keys() val recipients = participants.map(p => get(recipient_for_santa, p)) /// The initial state action init = a
Announcing: Learn TLA+
tl;dr: online TLA+ manual/advanced techniques/examples here. TLA+ is a tool for testing abstract software designs. I first stumbled on it in 2016 and found it so useful I wrote a free online guide to help others learn it. Then I decided the guide wasn’t good enough and wrote Practical TLA+ in 2018. Then I decided the book wasn’t good enough and needed a second edition. Just kidding! Book’s never g
Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch
Elasticsearch is a distributed search and analytics engine based on Apache Lucene. Initially released in 2010, it has quickly become the most popular enterprise search engine, and is commonly used for log analytics, full-text search, operational and security intelligence, business analytics, and metrics use cases. Built as a distributed system since its inception, Elasticsearch effortlessly scales
GitHub - afonsonf/tlaplus-graph-explorer: A static web application to explore and animate a TLA+ state graph.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
TLA+チートシート
日本語のTLA+に関する文献がほとんど見つからないので、日本語でまとめていきたいと思います。 誤った情報や追記したい情報などはこちらにIssueまたは、PRを送っていただけると助かります。 TLA+の勉強法・学習法 ドキュメントや講義など Leslie Lamport's TLA homepage: ホームページです。 Hyperbook: チュートリアルなどを扱ったHyperbookです。こちらのページからダウンロードが可能です。 TLA video course: TLA+の作者であるLamprtさんの動画教材です。 Specifying Systems: Leslie Lamportによるもので、出版社を通じての注文や個人使用のためのダウンロードにリンクしています。 Learn TLA もっとも詳細にTLA+及びPlusCalの文法や使い方について説明している場所です。現状唯一の情報
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
分散合意アルゴリズム Raft を TLA+ で検証する - 俺の Colimit を越えてゆけ
Using TLA+ in the Real World to Understand a Glibc Bug
TLA+の社内勉強会スライド公開します - takaha.siの技術メモ
Finding Goroutine Bugs with TLA+
qiita.com/blueband
www.buzzfeed.com
www.as-web.jp
news.yahoo.co.jp
health-literacy-info.hatenablog.com
buzzstyle-kei.hatenablog.com