サクサク読めて、アプリ限定の機能も多数！
トップへ戻る
買ってよかったもの
www.principia-m.com
CSP (Communicating Sequential Processes) の紹介資料 並行システムの理論 CSP (Communicating Sequential Processes) についての紹介資料を作成しました．並行システムの開発でポイントになる概念，逐次システムとの対比，CSP 理論の概要，検証手法とツールの紹介からなります． 並行システムの理論 CSP の紹介 (PDF, 2016/11/15 updated) 2016/11/19 に行われた「静的コード解析の会 第0回」で発表しました． http://metasepi.connpass.com/event/42141/ ビデオを撮っていただいたのですが，残念ながら音声がうまくとれなかったようです．再度紹介する機会があれば撮り直したいと思いますが... 「並行システムの理論 CSP の紹介」 on YouTube
セミナー 形式手法に関するセミナーを開催しています． 詳細につきましてはセミナーのページをご覧ください． SyncStitch: A Model Checker based on the Process Algebra CSP SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping: Deadlocks Divergences (also known as livelocks) Refinement relation on traces semantics (sa
Scheme で並行プログラミング言語を作ります．処理系は Gauche を使います． ここまでのおはなし 過去に興味がない前向きな方は次の節に進んでください．経緯を知らなくても本文は読めます． 2013年の Lisp Advent Calendar で「マクロとクロージャで作る並行プログラミング言語」という文書を書きました．並行プログラミング言語を定義して，マクロを使って Scheme に変換し実行できるようにしました．実行のために小さなオペレーティングシステムに相当するカーネルも作りました．並行プログラミング言語が簡単にできたのは，マクロのおかげに加えてクロージャと継続渡しスタイル (Continuation-Passing-Style, CPS) を使ったからです．カーネルのシステムコールは継続としてクロージャを渡すようになっていました． これらはとても便利である一方，少し課題もあり
2分探索が好きなんです。 「2分探索のコードなんか自分で書くな。ライブラリを使え。」 そうなんですけど、ちょっと次の問題を考えてみませんか？ 問題 プロポーショナルフォント（文字によって幅の異なるフォント）を使って文字列を表示するとき、与えられた幅に表示できる最大の文字列長を知りたいことがあります。 文字列の表示幅を計算してくれる関数 width(s, k) があるとしましょう。 ここで s は文字列、k は幅を計算する先頭からの部分文字列の長さです。 文字列 s の長さを s.len とすると、0 <= k <= s.len でなければなりません。 width(s, s.len) が文字列 s 全体の表示幅です。 width(s, 0) = 0 であるとします。 負の幅を持つ文字はないと仮定すると、width(s, k) は k に対して単調に増加することになります。 厳密には、幅 0
Structure and Interpretation of Computer Programs [1] （計算機プログラムの構造と解釈，以下 SICP）の第4章に，非決定的計算のためのオペレータ amb というものが出てきます．On Lisp [2] の第22章には choose と fail という同じく非決定的計算のためのオペレータが出てきます．元は Lisp の創案者である John McCarthy さんによって論文 [3] で紹介されたものだそうです．このオペレータを並列化してみようというのがこの文書の主題です． 言語はもちろん Scheme, 処理系は Gauche を使います． 非決定的選択オペレータ amb による天使の選択 非決定的計算も amb も初めて聞いたという人のためにかんたんに説明します．より詳しいことは SICP を見てください．パズルなど面白い例が出てい
弊社では並行システムの設計トレーニングプログラムを提供しています． システムのモデル化から設計検証，実装までを網羅した実践的なトレーニングプログラムです． モデル検査ツール SyncStitch を使用し，実際に手を動かすことでモデル化・検査・分析の技法を効率よく習得できます． 受講者の学習段階に応じた難易度の設定や学習テーマの選択が可能です． 短期集中，1日速攻コースなどのカスタマイズに応じられます． Skype による遠隔トレーニングが可能です．ご自宅等で効率よくトレーニングを受けられます． 特に以下の分野の方々に，ご専門の技術をブーストする技術を習得していただけます． 組込み技術者 マルチコア等による並列プログラムの開発者 マルチスレッドプログラミングの学習者 ネットワークアプリケーション開発者 システムの仕様策定者 テスト技術者 キーワード CSP (Communicating S
なんらかのデータを編集するためのユーザインターフェイスを持つアプリケーションプログラムで Undo/Redo を実現する１つの方法について書きたいと思います。 方法自体は一般的なものですが、ある条件を要求するので、残念ながらいつでも適用できるというわけにはいかないと思います。 いつでも適用できるようになるといいな、とは思っていますけど。 その条件とは何かというと、ユーザの操作に対応する遷移を、純粋に関数型で書くということです。 遷移を関数型で書く利点 SyncStitch のモデルは CSP に基づいた状態遷移モデルですから、全体としては関数型プログラムではありません（微妙なところですけど）。 しかし遷移において、状態変数やプロセスパラメータの値を計算する部分は純粋な関数型として記述します。 変数に格納されているデータ構造を副作用によって改変することはありません（できません）。 SyncS
Lisp から C 言語への変換器を作ってみたいと思います． 遊べる程度には機能があって，変換はできるだけ楽をするという方針でいきたいと思います． Lisp の仕様 まず入力となる Lisp の言語仕様を決めます． データ型 データ型はシンボル，整数（即値のみ），ペア，あと手続き（クロージャ）です． nil はシンボルで空リストと真偽値の偽を表すとします． 構文 構文を以下のように決めました． 定数リテラル 変数 (quote c) (lambda (var ...) body) (if test then else) (set! var expr) (begin form0 form1 ...) 関数適用 (fn arg ...) 細かいところは以下のようにします． 定数リテラルは整数のみ quote で指定できる式はシンボルか整数だけ．リストは cons で作る． lambda bod
Pthread Model Checker Pthread Model Checker の紹介 Pthread Model Checker によるデッドロック検出 Pthread Model Checker によるバリアの安全性検査 条件変数の Spurious Wakeups 生産者・消費者問題 1 生産者・消費者問題 2 生産者・消費者問題 3 生産者・消費者問題 4 ミューテックスと条件変数で作るセマフォ 1 ミューテックスと条件変数で作るセマフォ 2 ミューテックスと条件変数で作る rwlock スレッドプール 非決定的選択構文 AMB ワークスチール なぜ pthread_cond_wait はミューテックスを引数にとるのか Pthread Model Checker でペグソリティアを解く Translating C programs with POSIX thread int
Theorem Prover Advent Calendar 2013の参加エントリです． Lisp Advent Calendar 2013の方で，並行プロセスの理論 CSP (Communicating Sequential Processes) に基づいた小さな並行プログラミング言語を作りました． ここでは，その並行プログラミング言語の2つの意味，操作的意味と表示的意味を定義して，2つの意味論が同値であることを証明してみたいと思います． 並行プログラミング言語の構文 並行プログラミング言語の構文は次のようなものです．実装したものと少し変えました． プロセス式 ::= STOP | (! イベント プロセス式) | (alt プロセス式1 プロセス式2) | (par イベントリスト プロセス式1 プロセス式2) 変えたのは3カ所でです．1つは終了 SKIP の代わりに停止するプロセス
Lisp Advent Calendar 2013の参加エントリです． Lisp の特徴の1つとして，マクロを使って拡張言語（埋め込み言語）がかんたんに作れるという点があります． また Lisp はファーストクラスオブジェクトとしてのクロージャを持っており，継続渡しスタイル（Continuation-Passing Style, CPS）と組み合わせると，軽量プロセスがかんたんに作れるということもよく知られていると思います． そこで Lisp が持つこの2つの特徴を生かして，小さな並行プログラミング言語を作ってみたいと思います． 処理系は Gauche を使います．以下のモジュールを使います． CSP について ここで作る並行プログラミング言語は，CSP という理論を基礎にします． CSP とは Communicating Sequential Processes の略で，並行に動作するプ
Theorem Prover Advent Calendar 2013の参加エントリです． 定理証明支援系 Isabelle を使って，グラフの探索アルゴリズムの部分正当性証明をやってみたいと思います． 正確には単なる到達可能なノードの列挙ですけど，かんたんに探索へと改造できますので，よかったら遊んでください． 最近は Coq や Agda の話をよく見かけます．私はどちらも知らないので比較はできませんけど，Isabelle に興味を持つきっかけになれば幸いです． Isabelle について Isabelle は Larry Paulson, Tobias Nipkow, Makarius Wenzel らによって開発されている定理証明支援系です． HOL 一族の1つで，Standard ML で記述されています． 公式サイトはこちらになります： http://www.cl.cam.ac.
Think Stitch 最近の更新 2018/07/21 ソフトウェア開発を工学にする形式手法の紹介 2017/12/02 Dominators に関する定理の証明 2017/11/30 Pebbling a Chessboard 2017/11/26 Translating C programs with POSIX thread into CSP for refinement checking 2017/10/20 Pthread Model Checker でペグソリティアを解く 2017/10/15 なぜ pthread_cond_wait はミューテックスを引数にとるのか 2017/10/11 ワークスチール 2017/10/11 非決定的選択構文 AMB 2017/10/10 スレッドプール 2017/10/10 ミューテックスと条件変数で作る rwlock 2017/10/
かんたんな証明チェッカーを作ってみたいと思います． 関数はたったの7個です． まず1個目の関数が12,000行あります，なんてことはありません :P． 証明パズルとして楽しめると思います． この証明チェッカーは，David Gries さんと Fred B. Schneider さんによる本 A Logical Approach to Discrete Math （邦訳：コンピュータのための数学）を見ながら作りました． 公理と定理の番号はすべて本に合わせてあります． 等式論理 対象とする論理体系は等式論理とします． かんたんにするために命題だけを扱うことにして，述語や量化記号は扱いません． つまり命題等式論理ということです． もしかしたら等式論理というのはあまりなじみがないかもしれません． 正確なところは本などを見ていただくとして，しろうとなりに説明をすると，等号だけが述語で，それに関する
状態は単なる名前です．シンボルでも数でもよいとしておきます． 遷移ラベルは遷移を区別するためのラベルで，これもシンボルでも数でもよいとしておきます． 条件は遷移が可能かどうかを判定する論理式です．いわゆるガードです． 条件では変数宣言で宣言した変数が参照できるものとします． 変数変換は，この遷移が発生したときに，各変数の値がどのように変化するのかを指定する式です． ここでは話を簡単にするために，すべての変数の値をリストで返すものとします． 例えば変数宣言が ((x 0) (y 0)) となっていたら，同じ順序で x, y の値をリストにして返すものとします． モデル記述の全体と例 一般に状態マシンは複数ある（マルチプロセス）ので，リストで並べるものとします． モデルの全体例は次のようになります． (define m (make-model ((x 0) (p 0) (q 0)) ((P 0
条件変数のモデル “pthread_cond_wait はなぜミューテックスを引数にとるのか？” 条件変数のモデルを作ります。 ミューテックスのときと同じようにシステムコールをシミュレートしてモデルを作ります。 ※ こちらにある資料にも条件変数とミューテックスに関する詳しい説明とモデルがあります． はじめて pthead を勉強したとき、条件変数を待つ関数 pthread_cond_wait がなぜ条件変数の他にミューテックスを引数にとるのか不思議でした。 pthead を知っている人であれば、理由を知っている人が多いでしょう。 でも、出会いの運よく、疑問に思っていたけど理由は知らないという人がいたら、ここに来たのはラッキーです。 その理由を「お見せ」しましょう。 「本にそう書いてあったから」とか、「自分で考えてみて、なんとなくはわかるけど・・・」という人にも楽しんでもらえると思います。
惑星という言葉にはなぜ「惑」という字が使われているのか、ということについては中学生のときに理科で習いました。 プトレマイオスの頃は地球が宇宙の中心だと考えられていたと。 でもそうすると惑星がなんで行きつ戻りつ妙な動きをするのわからない。 しかたがないので周転円とかややこしいしくみを考えた。しかしうまくいかない。 そこにコペルニクスが現れて、地動説を唱えた。いやいや地球が動いてるんでしょと。 そうだとすると惑星が行きつ戻りつするのは地球が動いているからであって、惑星それ自体は太陽の周りを単純に回っているに過ぎないと。 その後ガリレオとかケプラー（とそのお師匠さんのティコ・ブラーエさん）がより精密な観測と計算をして、軌道は厳密には円ではなくて楕円だとか、面積速度の法則だとかを見つけます。 これらはみな、「運動とは何か」ということを理解するための探究だったわけです。 この問題に最終的に決着をつけ
このページを最初にブックマークしてみませんか？
『PRINCIPIA Limited』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
