Alignment in C
Alignment in C(Haase; 2014)https://wr.informatik.uni-hamburg.de/_media/teaching/wintersemester_2013_2014/epc-14-haase-svenhendrik-alignmentinc-paper.pdf CのAlignmentについての簡潔な説明である。
日本語の非常に詳細で有名な解説ページは下のものがある。 データ型のアラインメントとは何か，なぜ必要なのか？
ワードとはそのコンピュータが最も自然に扱えるビットサイズである、と定義されている。 この定義に従うと、メモリから一度に読み出せるビット幅、と多くの場合には一致することが期待できるだろう。 現在主流の環境である64-bitコンピュータではワードサイズは8byte(64bit)ということになる。
特殊なCPU命令を発行すると256bit幅を一度に処理することなどもあり、またもちろんchar型などのより小さなサイズのデータを扱うこともある。 Alignment制約とはこれらのワードサイズと異なるデータがメモリ上に配置される際に、効率的に処理されるようにデータを配置するようにCPUが要求する制約である。
例えば8byteのint型データがメモリ上で2つのワードにまたがって配置されていたとする。 このとき、メモリから一度に8byteの読み出しが可能であるにも関わらず、実際のデータの読み出しは2ワードの読み出しが必要になってしまう。
word a b c d e f g h memory ... | _ _ _ _ _ a b c | d e f g h _ _ _ | ...
一部の環境ではこのようなメモリアクセス(Alignment違反)に対して、実際に2ワードを読みだすこともあり、また他の環境ではエラーにさえなることもある。 具体的にはRISCアーキテクチャ、ARMやMIPSではalignment違反はエラーを送出するようだ。 特殊用途のSSE命令などでも、適切にalignされていないデータに対しての計算結果は定義されないことが多い。 現代的なアーキテクチャでは、misalignedなアドレスへのアクセスが可能になっているものもあり、多くの場合には2アクセスによって成されるため、性能の劣化がある。 (最近の?)x86_64ではこの性能的なペナルティ無しでmisalignedなアドレスへのアクセスが可能だそうだ。
また、stack領域のalignmentは環境により様々であり、例えばLinuxでは昔は4bytes, 最近は16bytes, Windowsでは4bytes, OSXでは16bytesだそう。クロスアーキテクチャで動作する必要のあるようなプログラムを書く際には注意が必要である。(具体的には、attribute*1や-mstackrealignなどを使いrealignmentを行うことで対処するそうである。)
note: * clangの-Wpaddedオプションを付けるとpaddingが入った時にwarningを出してくれるので、手動でメモリ使用量の最適化をかけるときに利用することができる * 構造体のpaddingを押しつぶすattribute*2, #pragma pack, -fpack-structなどの方法があるが、これはABIの互換性を壊すことに注意する必要がある * コンパイラが最適化の中でSSEの命令を発行するときには、適切にalignmentを保ってくれる(例えば16byte alignmentになるように適切にpaddingを入れる)はずであり、そのためプログラマが明示的に指示せずとも16bytes alignmentなどにデータが配置されていることがあるかもしれない
Planning with Specialized SAT Solvers(Rintanen; 2011)
Jussi Rintanenhttps://users.ics.aalto.fi/rintanen/jussi/氏のPlanning as SAThttps://users.ics.aalto.fi/rintanen/satplan.htmlに関連する一連の著作についてのメモである。
この論文Planning with Specialized SAT Solvershttps://users.ics.aalto.fi/rintanen/papers/Rintanen11aaai.pdfは古典的プランニング問題をSATに帰着し、ソルバを使ってSAT問題の解を計算し、その解から元のプランニング問題の解を抽出する、という枠組みの中で、汎用SATソルバではなく、プランニング問題のヒューリスティックを入れたソルバを構築することで既存の探索ベースのソルバを上回る性能を得たというものである。
汎用SATソルバではChaffなどで採用されていたVSIDSヒューリスティックスを使ったCDCL探索が主流である。 一方で、古典的プランニング問題の知識として、アクションの列を決定すると状態の遷移は一意に決定される、というものがある。 また、命題変数の中にはゴール命題という特に充足に対する要求が強い命題があり、これらの命題を充足するようなアクションを実行するような変数割当てはより有望であるといえる。 以上の2つの知識をSATソルバの変数選択に取り込むための仕組みを提案している。 (具体的な手法はFigure.1 Computation of supports for (sub)goalsを参照)
実験結果を見ると、充足解を計算する探索ベースのプランナのLAMA(IPC2008優勝)やYAHSPという当時state-of-the-artなプランナに対して、Mpという提案手法を採用したSATベースプランナがかなりよい性能を示していることがわかる。
Rintanenさんは一連のSATベースプランナの研究の中で、多くの手法を提案しており、これらの手法を取り込んだプランナがMpなのであるが、そのうちこの論文で提案しているPlanning問題のための独自ヒューリスティックを使わず、汎用SATソルバの変数選択ヒューリスティックVSIDSを採用したプランナMはLAMA, YAHSPにout-performされていることから、この論文で提案されている変数選択ヒューリスティックのプランニング問題への有効性が確認できる。
https://users.ics.aalto.fi/rintanen/satplan.htmlにある関連した面白い話としては、グラフアルゴリズムをプランニング問題に帰着することで作られた、より"プランニング色"の低い問題に関してはMがLAMA, YAHSP, Mpをout-performしているというものがある。 これはIPCプランニング問題のある種の"偏り"を示しているものと見ることができ、探索ベースのプランナやIPC問題に特化したプランナのチューニングの"脆さ"を示しているようで興味深い。
