Ansible/Vagrantでubuntuを起動してaptするときにdpkgのlockのエラーが出るやつへの対処

Ansible/Vagrantubuntuを立ち上げて、そこにaptで必要なものをインストールしたい*1ということはあると思うのだが、起動直後だとよく、「dpkgのlockファイルがあって実行できない」というメッセージが出て失敗してしまうことがある。無視すれば当然後ろの命令がうまく行かない。

Googleで「ansible ubuntu dpkg」でぐぐると、結構「dpkgのロックファイルを削除する」とか「killallでdpkgを殺してしまう」というようなどう考えても行儀のいいとは思えない対処法が出てくる。実は私も以前はそれをやっていて、大方はうまくいくのだが沢山やっていると失敗するやつが必ずあらわれて、それらのイレギュラーへの手動の対処が大変で「Infrastrcuture as a codeとは…」という気分になりやってられない。

そもそもこの原因は、Ubuntuがデフォルトだと起動時に自動アップデートをかけるのが原因なので、アップデートが終わるまで待ってからこちらのしたいことをすればいいのである。
そういうわけで、wait_for fails on apt-get / aptitude lock-file in /var/lib/dpkg/lock · Issue #16593 · ansible/ansible · GitHubのようなものも試したのだが、ロックファイルがどうもこれだけとも限らないようで成功率が100%にはならなかった。いまのところ、「そもそもdpkgが起動してるかをみるのが直接的でよくない?」ということで、今はもっぱら

 while ps -A | grep dpkg; do sleep 1; done;

を先頭に挟むことにしていて、今のところは成功率100%である。何かもっと筋の良い方法、常識などあったら教えてください。

*1:例えばvagrant awsubuntuインスタンスを立ち上げて、そのあとVagrantで操作できるように向こう側でpythonをインストールしたいとか

Visual Studio 2017でOpenCV 2.4.3をビルドする

諸事情によりOpenCVのバージョン2.4.3を使いたくなったのだが、バイナリの配布が終了していたのでVisual Studio 2017 (Community)ビルドしたくなった。そのときにコケたことがあったので(未だに全ての問題が解決したわけではないが)メモしておく。

  1. OpenCVgithubのtags(Tags · opencv/opencv · GitHub)から2.4.3を探しzipをダウンロード(https://github.com/opencv/opencv/archive/2.4.3.zip)。
  2. ダウンロードしたファイルを展開。
  3. CMake(https://cmake.org/)のWindows版を起動し、2で展開したディレクトリ(私の場合「C:/Users/ashia/Downloads/opencv-2.4.3」)を「Where is the source code」に、「Where to build the binaries」にそのなかのbuildフォルダを指定する(私の場合「C:/Users/ashia/Downloads/opencv-2.4.3/build」)を指定する。buildディレクトリは存在しないが、あとで確認の上自動で作られるので問題ない。
  4. 「Configure」をクリックしてOKとかをポチポチする(多分VS2017を使ってコンパイルする設定にデフォルトでなっていると思うが、なっていなければ直す)。CMakeがそのコンピュータのビルド環境を検出してくれる。
  5. 真ん中のおおきい窓にコンパイルオプション赤いリストが表示されるので、必要な機能に応じてつけたりけしたりするはずだが、今回の私の用途ではそのままにしておいた。
  6. 「Generate」をクリックする。CMakeがそのコンピュータのビルド環境を見て指定したbuildフォルダに、OpenCVをVS2017を使ってコンパイルするために必要なファイルを揃えてくれる。
  7. buildフォルダのなかにOpenCV.slnができているので、VS2017で開く。
  8. そのまま「ビルド>ソリューションのビルド」を実行するが、maxやminが未定義だと怒られるので、怒られているファイルのヘッダの先頭に「#include 」を付け加える。
  9. もう一度やるとさっきのエラーは消える。正直気持ち悪いのだが、私が今回使う機能には関係ない部分だったので無視していた。これでbuildのbinフォルダには(ビルドが成功した分の機能の)dllファイルができているし、libフォルダにはlibファイルができている。

拡張ユークリッド互除法を行列で書く

拡張ユークリッド互除法で実際に不定方程式の解を求めるとき、私は行列算で書くのが好きなのですがあんまりそういう解説を見掛けないのと、実は私もそれを思い出すのにいちいち20分ぐらいかかってしまうという理由でここにメモしておきます。

拡張ユークリッド互除法での「代入」

拡張ユークリッド互除法で 11a+7b=1なるa,bを求める方法は、通常次のように「代入」を用いて説明されます:
まず、

  • 11÷7=1 あまり 4
  • 7÷4=1 あまり 3
  • 4÷3=1 あまり 1
  • 3÷1=3 あまり 0

とあまりを計算する。これらのうち、「あまり=(gcd)」となっている式までを上から「あまり=わられる数-わる数×商」の形に書き直す。

  • 4 = 11-7×1 (イ)
  • 3 = 7-4×1 (ロ)
  • 1 = 4 - 3×1 (ハ)

となる。これを下から順に代入して、

  • 1 = 4 - 3×1 (ハを持ってくる)
  • = 4 - (7-4×1)×1 (ロを代入)
  • = (-1)×7 + 2×4 (整理する)
  • = (-1)×7 + 2×(11-7×1) (イを代入)
  • = 2×11 + (-3)×7 (整理する)

これで、a=2、b=(-3)と求まった。

行列で書いてみる

が、数に数を代入というのが気持ち悪いし、「整理する」のところで何を「係数」と見做して整理していいのかよく分からなくなるので、しばらくすると簡単にやり方を忘れて困ってしまう。そこで、これを行列算で書き直してみる。

ユークリッドの互除法では、(割られる数, 割る数)というペアから(割る数, あまり)というペアを計算するという操作を繰り返す。例えば上の例では、(11, 7)→(7, 3)→(3, 1)→(1, 0)となっている。
このペアに注目して、上の4本の式を行列算で書き直してみる。すると、次のようになる。

  •  \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}11\\7\end{pmatrix} = \begin{pmatrix}7\\4\end{pmatrix} (イ)
  •  \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}7\\4\end{pmatrix} = \begin{pmatrix}4\\3\end{pmatrix} (ロ)
  •  \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}4\\3\end{pmatrix} = \begin{pmatrix}3\\1\end{pmatrix} (ハ)
  •  \begin{pmatrix}0 & 1 \\\ 1 & -3\end{pmatrix}\begin{pmatrix}3\\1\end{pmatrix} = \begin{pmatrix}1\\0\end{pmatrix} (ニ)

ペアの第2要素は第1要素に移るので、係数行列の1行目はかならず(0, 1)になり、2行目はあまりを求めるところなので、(1, -商)となっている。
しらべたかったのは、(11, 7)に何をかけていくと(1, 0)にできるかということなので、まず(イ)の両辺に(ロ)の係数行列をかけてみる。すると、

  •  \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}11\\7\end{pmatrix} =\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix} \begin{pmatrix}7\\4\end{pmatrix} (イの両辺にロの行列をかける)
  •  =  \begin{pmatrix}4\\3\end{pmatrix} (ロを「代入」)

代入するにも、先の章とは違って行列の形が変な代入を防いでくれる。あとは同様のことをすればよく、少し考えると右から

  •  (ニの行列)(ハの行列)(ロの行列)(イの行列)\begin{pmatrix}11\\7\end{pmatrix} = \begin{pmatrix}1\\0\end{pmatrix}

となることがわかる。これはまさに我々がはじめ求めたかった形になっていて、答を求めるには左の行列積の連鎖を計算すればよい。

  •  (ニの行列)(ハの行列)(ロの行列)(イの行列)
  • =  \begin{pmatrix}0 & 1 \\\ 1 & -3\end{pmatrix} \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}
  • =  \begin{pmatrix}2 & -3 \\\ -7 & 11\end{pmatrix}

((ちなみにこれを手計算するときは2つずつ組にしてかけ算するとちょっと楽)あとはこの第1行をとって(あるいは両辺に(1, 0)をかけて)、a=2, b=-3がわかる。

まあこう覚えておくと、アルゴリズムにするときもちょっと思い出しやすいんじゃないかなあと思う。

論文ながしよみ「EXPERIENCE WITH STATIC PLC CODE ANALYSIS AT CERN」

Tsiplakiらの「EXPERIENCE WITH STATIC PLC CODE ANALYSIS AT CERN」をながしよみします。といいつつ、用語集を作ったら大体満足してしまったし、やってみた系の論文なのでそんなに内容はない。この界隈でどんな登場人物が出てくるかというまとめにはなった気がするので個人的には満足している。「この技法を産業応用してみたいぞ!」というときの参考にはなりそう。書誌情報はこちら:

@inproceedings{TsiplakiSpiliopoulou:2018avy,
author = "Tsiplaki Spiliopoulou, Christina and Blanco Viñuela,
Enrique and Fernández Adiego, Borja",
title = "{Experience with static PLC code analysis at CERN}",
booktitle = "{Proceedings, 16th International Conference on
Accelerator and Large Experimental Physics Control Systems
(ICALEPCS 2017): Barcelona, Spain, October 8-13, 2017}",
year = "2018",
pages = "THPHA160",
doi = "10.18429/JACoW-ICALEPCS2017-THPHA160",
SLACcitation = "%%CITATION = INSPIRE-1656449;%%"
}

用語集(しらべたり知ってることを書いたりしている。割と適当。)

  • PLC: Programming Logic Controller。工場の機械を制御するのによく使われている制御装置(の規格?)。工業用や宇宙用の丈夫なArduinoだと思っている。このためのプログラミング言語*1があり、SiemensのSCLやSchneiderのSTといったものがある。もともとリレーをたくさん並べて機械を管理していたのをリッチにしていったらプログラミング言語になったみたいなやつらしい。この論文ではこの言語のことをPLC program languageとよんでいる。IEC 61131-3 標準規格で規格化されている。日本だとオムロンがやってるらしい。
  • SCL: PLC用のプログラミング言語Siemensが作っているらしい。CERNではSCLを使っていて、この論文もこちらを対象にする。
  • UNICOS: UNified Industrial COntrol System。LHC(Large Hadron Collider, 大型ハドロン衝突型加速器)を制御するためのフレームワーク。この上でPLCの開発ができるらしい。 https://cds.cern.ch/record/1402490/files/WEPKS006.pdf?version=1
  • static analysis: 静的解析。コードを解析して、そのコードを実際に実行することなくそのコードの性質(無限ループに落ちないかとか変なメモリ操作をしてないかとか)を調べること。プログラムの品質保証の技法としてよくテストなんかと対にされる。
  • model checking: モデル検査。コードから数学的対象(大体ある種のオートマトン)を取り出して、その数学的対象を数学的に調べることでもとのコードの性質を調べる静的解析の一手法。コードについて網羅的に何かを調べることができてよい。
  • PLCverif: PLC用のモデル検査器。CERNで作られたらしい。 http://ddarvas.web.cern.ch/ddarvas/publications/icalepcs2015/WEPGF092.pdf
  • FB: function block。PLC言語での関数に相当するぽい。
  • IM: intermediate representation。PLCverifはSCLのコードを一旦中間表現に変換する。
  • CFG: control flow graph。オートマトンの一種で、普通の手続き型プログラムにオートマトン的な解析をしたいときは大体これに変換する。大体プログラムの各行がCFGの1状態に対応し、それらの遷移に条件分岐や代入の情報が載っていると思えばよいと思う。
  • nuXmv: モデル検査器。https://nuxmv.fbk.eu/で公開されている。有名なモデル検査器としてNuSMVがあるが*2、これにSAT/SMTソルバとの連携をくっつけたものらしい。
  • CBMC: C言語/C++用の有界*3モデル検査器。https://www.cprover.org/cbmc/から入手できる。Oxfordのグループが作っている。結構産業応用に意欲的で、そのために地味なことを高品質でやっているイメージがある。
  • Xtext: プログラミング言語(特にDSL?)のための開発環境開発のためのフレームワークらしい。https://www.eclipse.org/Xtext/から入手できる。対象となるプログラミング言語の文法を書いてXtextに与えると、パーサ、コンパイラ、その言語のためのEclipse拡張、各種エディタ拡張が生成されるらしい。

アブストアブスト

CERNで使われているPLCのやばそうなところを見つけるために、主に普通のプログラミング言語に使われている静的コード解析の技法を使ってみます。使ってみたツールややってみた経験を共有します。

内容

PLCverifを利用している。まずPLCverifの簡単な説明をしている。

PLCverifの説明

Figure2に書いてあるが、SCLのコードが与えられると、これは中間表現に変換される。このために、Xtext(というかXtextで生成されたツール)を使ってSCLコードをパースし、抽象構文木(AST)を得る。ASTの構造はFigure3に示されている。PLCverifには、このASTを解析するための「ルール」が定義されていて、その「ルール」に従っているか、あるいはviolateしているかを教えてくれるらしい。

適用例

この解析では、コードのやばい匂い(code smell)をみつけることを目的としていて、そのための「ルール」を検査している。この論文中ではうち2つの「UNICOS naming convention rule」と「Nested conditional if statements rule」を紹介している。

はじめの「UNICOS naming convention rule」は、変数名がUNICOSの命名規則(Table1)にしたがっているかを検査する。たとえば、Figure4のコード中の「AuMoSt」は、「Auto」をあらわす略語「Au」、「Mode」をあらわす「Mo」、「Status」をあらわす「St」を組合せたもので、これらの略称はちゃんと表のなかにあるので大丈夫だが、2行目の「E_FuStopI」は「Fu」が表にないので駄目である。

次の「Nested conditional if statements rule」は、深いIf文について警告を出すらしい。このルールはFigure5に示されている。

感想

タイトルで「Experience」と言っているとはいえもうちょっと検証の論文だと思っていたが、かなりソフトウェアエンジニアリングの論文でした。特に検証技法的に面白いところはなかったように思うのですが、エンジニアリング的には面白いんでしょうか…

よくわからんところ

  • ここに書いてある「ルール」の検査だけだとCBMCもnuXmvもいらなそうなんですがどこで使ったんですか

英語的に勉強になったところ

  • 「The large number of industrial control systems based on PLCs (Programmable Logic Controllers) available at CERN implies a huge number of programs and lines of code.」っていうんですが、implyに物理的な「含む」っていう意味あったんですか

*1:チューリング完全かどうかは知らない…

*2:この界隈では珍しく和書の入門書が産総研から「モデル検査 初級編―基礎から実践まで4日で学べる (CVS教程)」として出ている。

*3:普通モデル検査というと無限ループのような無限の挙動を扱うことができるが、有界モデル検査ではループはある程度大きい定数回の繰り返しに展開されてしまう。

duneでwarningが全部errorになってしまうのをなんとかする

OCamlの(多分次期標準の)ビルドツールであるdune(https://github.com/ocaml/dune)を使ってコンパイルすると、すべてのwarningがerror扱いされてしまいます。例えば、


について

dune exec ./main.exe

を叩くと、

ocamlc .main.eobjs/main.{cmi,cmo,cmt} (exit 2)
(中略)
File "main.ml", line 2, characters 6-7:
Error (warning 26): unused variable x.

となり、未使用変数の警告がエラー扱いされてしまって実行することができません。どうもduneがocamlc(コンパイラ)にwarningすべてをerrorにする「-w @A」をわたしているようです。開発中の未使用変数ぐらい大目に見てほしいので、warningのままでいてほしいです。そこで、duneファイルを

として、ocamlcにさらにwarningすべてをerrorとして扱わない「-warn-error a」を渡すと解決します。

http://ocaml.jp/archive/ocaml-manual-3.06-ja/manual025.html

(ところで、gistで1ファイルだけ埋め込むときはgistの上のほうの埋め込みタグのURIの後ろに「?file=hoge.fuga」をつければいいのね)

横内寛文「プログラム意味論」を流し読みした

本当は読書メータの感想のところに書こうと思ったのだが字数が溢れてしまったのでここに書いておく。
あんまり真面目に読んでないんだ、ごめんね。


気にはなっていたのだか積読で、一念発起して興味あるところだけ読むことにした。そういうわけで全体の話はしてません。

公理的意味論は(他の意味論のスタイルと明確な区別があるわけではないが)プログラムの構文に、その文が意味する数学的対象を直接割り付けるもの。プログラムが停止しないなどのエラーをうまく扱えるその数学的対象としては部分関数が便利で、その順序をうまく扱うためにcpo(complete partial order)という順序集合のクラスを用いる。そうするとこの上で不動点の議論ができ、それが再帰やwhile文といった自明には意味が定義できないものにも意味を割り付けることができる。この議論の後に、λにいくらかの基本型と再帰を許す関数定義μを追加したPCF(Programming language for Computable Function)を定義し、それに対して意味論を与える。

型なしラムダ計算に公理的意味論を与えるのに素朴に集合論で言うところの関数を割り当てようとすると、自由な関数適用のせいで矛盾が起こってしまう。これに対処するには、X→Xの関数がXに埋め込めるようなcpo Xを見つけなければいけない。このような要求を方程式風に書くとX=[X→X]というようになるが、このようなcpoの対象についての方程式を領域方程式という。この方程式の解が見つかれば、そこから型なしラムダ計算の意味論(モデル?)を作ることができるが、実際この解として2点以上の集合Dから埋め込みを繰り返して無限直積を取り作ったcpoであるD∞が解であることを確かめる。なお、この領域方程式を解く方法を研究したり、この状況をcpoだけではなくω-完全な圏でのcolimitを考えて本質を捉えようとするというような議論もこの本ではなされているが、とりあえず具体に興味があったのでそこは読まなかった。

疑問として、そんな風にして意味論を作ってそれで「型なしラムダ計算の理解が深まった」と言えるのか、普通にラムダ式を適当な同値関係で割ったものそのものを眺めるのと比べて何かいいのかという疑問は残ったが、真面目に読んでないからかもしれない。

(8/27追記)公理的意味論がつけば、(λx.xx)(λx.xx)に⊥が対応することがわかるよと教えてもらいました。そういう意味では公理的意味論は数学で言うところの不変量みたいな感じで使えるんですね。

OCamlのwith typeの使い方を失敗から学んだ話(ファンクタシグネチャの返り値でモジュールを制限したくなったときどうすればよいか)

OCamlでのSetの使い方がよくわからない(どれがいいんでしょう) - ashiato45の日記に引き続き、有限オートマトンOCamlで記述することを考えます(前の記事は読んでなくても大丈夫です)。今回は文字列を読んで受理拒否を判定する関数は載せず、純粋に有限オートマトンのデータ構造を提供することを考えます。ただし、アルファベットと状態をあらわす値は好きなものを選べるように、ジェネリック的にしたいとしましょう。
2.3 ファンクタなんかを参考にしながら書くとこんな感じになります。
gist.github.com

これで良さそうな気もするのですがここでさらに、ファンクタAutomに具体的によく使う集合を与えて、具体的なオートマトンのモジュールも作ってこのライブラリで提供することを考えましょう。次のように書いてみます。
gist.github.com
今回はZeroとOneを持っているalph型を定義し、その集合をアルファベット集合AlphSetにします。状態集合は文字列集合StringSetということにします。そしてこれらをAutomファンクタに与え、ZeroOneAutomモジュールを作ります(autom_dame2.mliの19行目)。モジュールはシグネチャで制限してインターフェースを提供してやらないことには外部からアクセスできませんので、4行目で定義したファンクタシグネチャAUTOMを使って

module ZeroOneAutom: AUTOM(AlphSet)(StringSet)

と制約することを考えます…が、これはコンパイルエラーになります。文法が定義してあるOCamlの公式マニュアルの
7.10  Module types (module specifications)を見てみると、そもそもこういう書き方はできず、コロンの右側には基本的にはシグネチャを置かなければならないということがわかります。

そこで、仕方がないのでファンクタで帰ってくるものだけを取り出して書き(以下AUTOM')、AUTOMはAUTOM'を返すようにすることを考えてみます。
gist.github.com
ただし、AUTOM'の定義のときには引数のモジュールの情報は使えませんので、とりあえず必要な型だけをast, sst, aset, ssetとして定義しておいて、それを使って全体を定義しておきます(autom_ok.mliの4-15行目)。そして、AUTOMの定義のなかでwith typeを使って、AUTOM'で仮置きした型と、得られたモジュールの型とが一致するという制約をかけます。これで、ZeroOneAtomはAUTOM'シグネチャとtype withを使って無事制限をかけることができました。ついでに、AlphSetとStringSetも外部からきちんとアクセスできるようにtype withで制約をかけてあります。type withのはたらきですが、merlinの表示する情報を見るのがわかりやすい気がします。

module ZeroOneAutom: AUTOM'
with type ast = AlphSet.t
with type sst = StringSet.t
with type aset = AlphSet.Elt.t
with type sset = StringSet.Elt.t

の情報をmerlinで表示させると、次のようになります

sig
type ast = AlphSet.t
type sst = StringSet.t
type sset = StringSet.Elt.t
type aset = AlphSet.Elt.t
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

対して、

module ZeroOneAutom: AUTOM'

の情報は

sig
type ast
type sst
type sset
type aset
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

となります。このように、type withを使うと、型の後ろにイコールとその型が何かを追加することができるようです。このことを「シグネチャに型の等価性情報を追加する」というようです*1

ちなみに、先の文法のページ(2.4 ファンクタを使った型の抽象化])を見ていたところ、type withならぬmodule withというのもあるようだったので、これも試してみました。すると、次のようになります。
gist.github.com
「module with M = M2」のようにすることで、AUTOM'シグネチャ内で仮置きしたAlphSetモジュールとStateSetモジュールに(autom_ok2.mliの5、6行目)、モジュールの等価性情報を追加することができています(行18、19や30、31)。実際、

module ZeroOneAutom: AUTOM'
with module AlphSet = AlphSet
with module StateSet = StringSet

の情報をmerlinで見てみると、

sig
module AlphSet :
sig
module Elt :
sig
type t = alph
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
val sexp_of_t : t -> Ppx_sexp_conv_lib.Sexp.t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
module StateSet :
sig
module Elt :
sig
type t = string
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
type t = {
alph : AlphSet.t;
states : StateSet.t;
trans : StateSet.Elt.t -> AlphSet.Elt.t -> StateSet.Elt.t;
init : StateSet.Elt.t;
final : StateSet.t;
}
end

となっており、確かになかのAlphSetやStateSetにmodule withで与えたAlphSet(これは外側のalph型のためのモジュールの名前!)やStringSetの情報が反映されていることがわかります。