書評: ビッグデータを支える技術

Googleを支える技術 ?巨大システムの内側の世界 (WEB+DB PRESSプラスシリーズ)で著名な西田さんの著書である。とても先見性のある本で、当時は仕事でもあったからとてもお世話になった。その西田さんの新作だというし、最近はもういろいろビッグデータのソフトウェアとミドルウェアがありすぎてワケの分からないことになっていると思ったので、知識を整理するためにサクッと購入。

ビッグデータを支える技術―刻々とデータが脈打つ自動化の世界 (WEB+DB PRESS plus)

ビッグデータを支える技術―刻々とデータが脈打つ自動化の世界 (WEB+DB PRESS plus)

本書の冒頭でも触れられているが、昨今ではありとあらゆるソフトウェアがオープンソースで公開されているし、詳しい情報はほぼすべてインターネットで公開されているから、この本はカタログ的にさまざまな概念や製品を紹介していき、個別に深く解説することはしないと注意されている。まさにそれこそが本書の価値で、元エンジニアで昨今のビッグデータの潮流を知りたい課長、部長級の管理職や、現場でビッグデータを前に呆然としているエース級のフルスタックエンジニアが知識の補完を行う用途にピッタリである。次点で向いている用途としては、これからビッグデータの赤い荒波に乗り出していこうと考えているエンジニアや営業職にとっても、業界を俯瞰して全体図を把握するにはよい（当然コレだけではダメで、そこから自分の得意分野を深掘りしていかなければならないだろう）。ビッグデータのことが分からない、という人は必読の一冊だ。

私自身はこの業界にもう10年近くいることになるので、おおよその概観を脳内に持っているつもりだったが、思った以上にビジネスインテリジェンスとかETLとかバッチとかに多様な世界があって、いろいろあるらしいなあということをざっと確認できたのでよかった。以下は、自分の専門分野で気になったところの指摘をささやかながらしておこうと思う。ちょっと忌々しい指摘ではあるが、これで本書の価値が損なわれるわけではないのでお間違いのなきよう。

10/6追記: YARNとLXCに関して - 「ビッグデータを支える技術」補足 にて捕捉いただいた。この捕捉を読んでから、以下のコメントは割り引いて読んでいただきたい。

Apache Mesos について @ P119

119ページのカラムで「Mesosによるリソース管理」と題してApache Mesosの紹介をしているのだが、2017年の本にしては情報が古い。まず出だしの「MesosはOSレベルの仮想化技術を用いており、YARNと比べると…」という話からしてアレでして、YARNもMesosもリソース制限は基本的にcgroupを使っているわけなのでそんなに変わらない。Namespacesの利用があるかどうかは異なるかもしれないが、それはリソース制御ではなくIsolationなのでちょっと違う。また「Dockerと同じくLinuxコンテナ（LXC）が用いられ」というのは明らかに誤り。遅くても1.0の時点でサポートされているコンテナエンジンはDockerかMesos独自のエンジンであり、LXCは一年以上前から利用していない。DockerもLXCは既に利用しておらず、LinuxのNamespacesを利用している。

またその後の解説でMesosにData localityがなく、一方でYARNにはあるのでYARNの方が優れていると解説されている。確かにMapReduceなどのLocality機能と親和性が高い機能がYARNだとスムーズに動作するらしいが、Mesosの2 level scheduler という思想に基づけば入力データのHDFS上の位置をみつつLocality awareに作るのはフレームワーク側の仕事である。テクニカルには、多数のOfferを抱えておけばIPアドレスは分かるので、フレームワーク側でデータの位置と割り当てられたリソースをマッチングしてスケジュールすることが可能。むしろYARNみたいに中央集権的にスケジューリングするよりも、Mesos用にスケジューリングアルゴリズムを自律的に使い分ける方が便利なケースもあるだろうから、Data localityがあるから優れていると一方的に評するべきではない。それでも、On the flyですぐLocalityを考慮してジョブを動かせるのは便利だけど、それは計算フレームワーク側が対応してるかどうかの問題じゃないかと思う。もちろんYARNの方が対応してるソフトウェアは多いと思うが、それは個別のソフトウェアの話だろう。

分散システムという言葉について

また、本書の全体を通して「分散システム」という言葉が定義なしに使われていて、都度どのような故障モデルや通信モデルを備えているのか、合意の基準は何なのかが引っかかる。

特にP150では「TCPではメッセージにシーケンス番号を付けますが、分散システムではシーケンス番号はあまり使われません」と表記していて、続く文章で欠番のないシーケンス番号の発行は（いわゆる故障あり非同期通信モデルでは）現実的に難しいためと解説している。たしかにトランザクションIDやTCPのシーケンス番号、REDOログなど欠番があったときに途中のメッセージを待つ必要がある場合には、要件を満たすシーケンス番号を発行することが技術的に難しい（Twitter の Snowflake などはあったが、それだけでクラスタを一つ組まなければならない）ので「使われません」という表現になる。なる、が、非常にこれはミスリーディングで、我々がシステムで依存しているPaxos, Zab, Raft といった分散合意プロトコルは欠番を許容するシーケンス番号を順につけていって、プロトコルの正しさはその順序性に依存しているのである。Raftはシーケンス番号の欠番を許さないが、欠けたデータを復元する手順を持っている。

この言い回しが紛らわしいのは「分散システムでは」の主語が大きいことに由来しているので、もっと限定的に書くべきであった。そもそもこの文章はストリーム処理における "at least once" の解説に含まれている場面であって、冗送排除の文脈であって欠損メッセージの検出ではない。したがって同じメッセージには同じIDがついているだけで十分で、送信側が受信側からAckを確認するまで再送し続ければ at least once は達成できる。つまり欠損の検出が不要なわけで、シーケンス番号じゃなくてもいい…シーケンス番号はよく使うんだよ…という主張だ。「あまり使いません」というミスリードは不要だったのではないかという話。

最近のBashoのニュースの「買収」という言葉はちょっと違う（追記あり）

PublickeyというIT界隈でわりと影響力のあるサイトで分散型NoSQLデータベースの「Basho」をギャンブルサイトの「Bet365」が買収。全製品のオープンソース化を表明という記事が公開された。しかしながらこの記事は若干の誤りを含みつつミスリードが多かったのでここで指摘していきたいと思う（この記事の公開後に修正あり）。今北産業の方々は末尾のまとめをご覧いただきたい。

www.publickey1.jp

なお私は 2016年3月までBashoの日本法人の被雇用者であり機密情報を一部知る立場であったが、ここでは公開情報だけをもとに解説する。また現在は一連の関係者との公的な関係は一切なく利害関係にないことを明記しておく。つまり外野で野次馬です。

基本的な指摘事項

Bet365を表現するのに「ギャンブルサイト」という言葉は一般的ではない、きちんとした会社である（対応済み）

はてブでブックメーカーをギャンブルサイトといえば確かにそうだけど。というコメントがついている通り、Bet365は伝統的なブックメーカーのオンライン版であると表現するのが正しい。「アメリカの大統領選挙やゲームの大会、アカデミー賞の授賞者や次のジェームズ・ボンドを演じる役者等もブッキングの対象になる」とあるように、イギリスではプレミアリーグから何から何までギャンブルの対象にすることが法律で認められている。飲み屋でよくある「アイツが明日遅刻するのに10ポンド賭けてもいいぜ」みたいなのが大っぴらにできるというわけだ。日本では賭博行為は一部の公営のものだけが認められており、その他の賭博は全て違法である。日本語で「ギャンブル」というときはネガティブな文脈で出ることが多く、関連付けて記述されたものはよい迷惑であろう。

こちらの解説にもあるようにBet365はきちんとした歴史ある会社で知名度も高い。

BET365とは1974年から続く超老舗ブックメーカーで、 現在は、全世界200ヵ国に500万人の顧客がいる と言われている大手メーカーです。
イングランドプレミアリーグ(イギリスのトップリーグ)、ストークシティのユニフォームスポンサーを務めるなど、名実ともに信頼ある大企業です。

しかるにPublickeyではタイトルからしてミスリーディングであり、Riakというソフトウェアの将来が怪しいギャンブル企業に買われてしまってどうなってしまうのか分からない…といったことを示唆する記事になっている。もちろん本文にそういった記述はないが、日本での賭博行為に対する一般的なイメージからいって先入観をもって読まれることは確実であろう。

したがって、新野さんは何よりもそれを予め防ぐような書き方をすべきであったと思います。訂正入りました

Riakを始めとするBashoの製品は「ほとんど」がそもそもオープンソースソフトウェアであった（対応済み）

記事には「Bet365のCTOが、Bashoの全製品をオープンソース化すると宣言」という見出しがあり、この曖昧な記述ではBashoの製品がプロプライエタリであるかどうかはっきりしない。全製品をオープンソース化という表現は、全製品がクローズドソースであったことを強く示唆する書き方であり、Riakというソフトウェアの正しい理解を妨げると思う。もともとRiakはOSS版とプロプライエタリ版があり、OSS版では一部機能が実装されていないという差があっただけのことだ。それはPublickeyの以前の記事（Amazon S3互換、Yahoo! Japanも採用した分散オブジェクトストレージのRiak CSがオープンソースで公開 － Publickey）でもある程度触れられていると思ったのだが、ここの記述は簡素に過ぎると思う。

OSS版との機能差は主に以下である。

  1. データセンター間レプリケーション
  2. SNMP/JMXによる監視機能

SNMPなどはまあオマケで、基本的にこのデータセンター間レプリケーションが目玉であったため、ここだけはソースコードは公開されていなかった。OSS部分は実に膨大で、ソフトウェアの機能でいうと9割以上はOSSとして公開されていたといっていい。いちおうここに機能差の表がある（が、いつまで残っているかはBet365次第だろう）。

Bashoの資産はソースコードだけではないし、全ての資産を買収したわけでもない（対応済み）

Bashoの資産は商用版のソースコードだけでなく、他にも多くのものがある。

  1. 既存アカウントとのサポート契約
  2. basho.com のドメインと関連するインターネットサービス（ *.basho.com のWebサイトや riak-users などのML）
  3. GitHubアカウントや、Bashoが持っていた各種データ、ログ、ビルド関連のツールやサーバーなど
  4. Riakの商標権

たとえばRiakのドキュメント docs.basho.com はしばらく前から利用できなくなっていたし、 RiakのカンファレンスRICONのサイト ricon.io も今はアクセスできくなっている。RiconはRiakに限らない分散システムのカンファレンスを標榜していて、Riakに限らず分散オタクたちのハードコアなカンファレンスとして有名であった（こういうやつ）。まあGitHubアカウントやいろいろな性能や試験などのソフトウェアに関するデータはそのうち出てくるかもしれないし、Bet365が不要だと判断して破棄するかもしれない。

なかんづく重要なのはRiakの商標権で、これについてスレッドでも盛り上がっていた。商標権を確保しているといないとではOSSとしてのRiakの使いやすさが大きく違う。もちろん商標がなくてもライセンスで認められているのでOSSとしてソフトウェアを利用し続けることはできるが、Riakそのものを使ってビジネスをすることが難しくなるし、OSSとして好ましい状態ではない。Hudsonのことを覚えておられる読者諸賢も多いのではないだろうか？

最後の問題点は既存アカウントとのサポート契約だ。Bet365の人からのメールにも "Basho's remaining assets (except support contracts)" と明記されている。つまり厳密には「Bet365とBashoは、Bashoの資産をすべてBet365が買収することで合意」という表現も誤っている。

私の推測では、Bet365の動機はこの商標権とデータセンター間レプリケーションなのではないかと思う。データセンター間レプリケーションは長年の大型クラスタでの無停止運用にも耐えた実績があり、こちらをうまくコミュニティで共同でメンテナンスすることで使い続けたいという意図がOSS化の背景にあると想像している。

「買収」の背景: これはいわゆる普通のスタートアップの買収とは違う

さてRiakやBashoという名前、昨年はほとんどインターネット上で見かけることもなかったと思う。今年に入ってからはめっきり動きがなくなり"Will the last person at Basho please turn out the lights?" と、その消えっぷりに疑問を持つ人が多くいたくらいだ。これが 7/13 で、その月末には End of the road for Basho: Court puts biz into receivership • The Register という記事が出ており、 "filed for receivership in early July after Basho defaulted on payments" と書かれている。つまり資金繰りができなくなって7月にreceivership状態になった（何と訳すのがよいか知らないが「管財申請」とか財産管理状態ということだろう）。Wikipediaによると破産すらできない状態ということらしい。こうなると具体的にどういうプロセスを経ていくのかは詳しくはないので分からないが、こういう状態であるから、いわゆるスタートアップの買収とは異なり人もモノもないので、二束三文の価格だったのだろうと容易に推測できる。つまりBashoに投資した投資家は大損こいたわけである（あれ、Receivershipになったということは投資家には二束三文どころか1セントも戻らないということ？アメリカの制度詳しくないので誰かに教えてほしい）。これは救済とは呼べない。

実際に世界中のオフィスが閉鎖され、ほとんどの従業員が既に解雇されており、Bashoの良心たるMvMが Basho closed とメッセージを発信していた。さてこれで困るのは大規模なRiakクラスタを抱えるユーザーたちである。データセンター間レプリケーションを除くほぼ全ての機能はソースコードが公開されているからすぐには困らないものの、ソフトウェアをメンテナンスしながら使い続けるか、他のソフトウェアに移行するかを選ばなければならない。後者は基本的に黙って去るので、特にインターネット上で観測できない。前者はBet365を筆頭に、BashoとRiakの技術を高く買っているところが集まったようだ。6月にはErlang Solutionsが商用サポートの検討を始め、8月の時点で商用サポートが行われることがアナウンスされた。- Erlang SolutionsのRiakページ によるとRiak CSもサポート対象のようだ。おおお。。。

NHSは商用版に諦めをつけ始めたのか、データセンター間レプリケーションのミドルウェアをRabbitMQを使って作ってしまったようだ（公開直後にBet365のニュースを知って驚いたともコメントしている）。

Riakはこれからどうなるのか？

コミュ二ティでは、Bet365、Erlang Solutions, NHS を中心にメンテナンスが続けられていくだろう。公開予定の商用版コードについてはApache 2ライセンスが支持されているようだ。その場合、Bashoなき今、著作権者は誰になるのだろうか？　素直に Apache 財団に送ってもよいと個人的には思うが、みんなJIRA嫌いだったしなあ…CNCFってこともないだろうしな…

商用サポートについては、アナウンス通りTI Tokyoという東京の会社がサポート契約を買い取っており、既存顧客のサポートはそちらでErlang Solutionsと共同で行われる模様だ。
あとのことは分からない。

まとめ

  • Bet365は「ギャンブルサイト」ではなく伝統的なブックメーカーであり、合法で社会的に認められた事業である
  • 「全製品をオープンソース化」ではなく、これまでプロプライエタリだった部分を公開するとBet365が宣言した
  • Bashoの資産はソースコードの他にもいろいろあって一番不安視されていたのが商標権
  • これはいわゆる普通のスタートアップ買収とは異なるものであるが「救済」という言葉も少し違うと思う

追記: その後コメントをいただき、記事が修正された。時間をみるにわたしが記事を公開した直後の対応だったようだ。

参考

Replication (Lecture Notes in Computer Science)

Replication (Lecture Notes in Computer Science)

Real World HTTP ―歴史とコードに学ぶインターネットとウェブ技術

Real World HTTP ―歴史とコードに学ぶインターネットとウェブ技術

ハイパフォーマンス ブラウザネットワーキング ―ネットワークアプリケーションのためのパフォーマンス最適化

ハイパフォーマンス ブラウザネットワーキング ―ネットワークアプリケーションのためのパフォーマンス最適化

2017年冬〜春アニメまとめ

anime

概要

冬は「この素晴らしき世界に祝福を！２」「CHAOS;CHILD」くらいしか面白いものがなくて不作であった…と思ったら、あとで追いついた幼女戦記がここ一番の出来だった。。春は完走は多かったものの「有頂天家族２」が突出していてベルセルク2期は安定、次点は「つぐもも」か。

リアルタイムではないが2017年上半期に後から完走したものとして「響け！ユーフォニアム」2期、東京喰種√A、青の払魔師、この素晴らしき世界に祝福を！、SAOおよびSAO2、有頂天家族1期、幼女戦記、Charlotteなどが高評価だった。

個別

昨年秋アニメも残していないものがいくつかあったので合祀。面白いところはネタバレしないように気をつけています。

  • 無星: 見る価値がない。一応完走
  • ★: 一度は見ておいた方がよい
  • ★★: もう一度見返しておきたい
  • ★★★: 他人に自信をもって勧めたいレベル

幼女戦記　★★★

前世紀の魔法大戦物だけど、転生もの。空戦の描写はハリウッド的で迫力があってSEもよい。なんとも言えぬ閉塞感の中でとにかく勝ちまくるのが非常に気持ちがよい。帝国が滅ぶところが全然想像できない。アニメでは時間が足りなかったが、漫画だとすれ違いが強調されていてこれは別にまた面白い。2017年上半期個人的No.1をあげたい。

eYe's 【通常盤】

eYe's 【通常盤】


オープニングテーマが非常に気に入ったのでアルバムを買ったら、Re:ゼロでもいくつか曲提供している人たちだった。

ゼロから始める魔法の書

傭兵とゼロの魔法の国のお話。国が案外小さいのと、ゼロの魔術師団があまり賢くなくて悲しい。傭兵のハイパー超人クライミング技術はすごいんじゃないかと思う。

終末何してますか？忙しいですか？救ってもらっていいですか？

ようわからんかった…原作みたら面白いと思えるのかもしれないけど、ファンタジー度が高くて俺には難しそう。ヒロインが14、15歳なのに結婚とかいうのもちょっとオッサンにはきつい。

ソートオラトリア　ダンまち外伝

ダンまちが面白かっただけにちょっと残念。59階層に着いて終わりで、アイズの正体は生い立ちに切り込んでからが面白そうなのだけど、2期がちょっとなさそうな感じ…

有頂天家族２ ★★★

狸一家の心温まるドタバタ喜劇に、天狗親子の確執と愛情を織り交ぜてより面白くなった。

有頂天家族　二代目の帰朝 (幻冬舎文庫)

有頂天家族　二代目の帰朝 (幻冬舎文庫)

有頂天家族 ★★★

狸一家の心温まるドタバタ喜劇。ウィットのある会話と話のおかしさと家族の絆がとてもよい。優しくなれるお話

有頂天家族 (幻冬舎文庫)

有頂天家族 (幻冬舎文庫)

武装少女マキャベリズム

武闘派学園ハーレムもの。

ベルセルク2期 ★★

安定。断罪の塔編終了後から

ベルセルク 39 (ヤングアニマルコミックス)

ベルセルク 39 (ヤングアニマルコミックス)

ロクでなし魔術講師と禁忌教典 ★

肌の露出多い以外はなかなか面白い魔法学園もの。主人公がやる気がないっていう典型的なところが感情移入できてすばらしい。結局アカシックレコードのカケラも出てこなかったが、二期は厳しそう。

つぐもも ★★

軽快でテンポのよい定番コメディ。戦闘シーンはまあまあ迫力があるし、主人公の成長もよい。今思ったけど、かなり「かんなぎ」にクリソツじゃね…？

この素晴らしい世界に祝福を！２ ★★

安心してゲラゲラ笑いながら見れるのでよい

この素晴らしい世界に祝福を！ ★★

ゲラゲラ笑いながら見れるのでよい

CHAOS;CHILD

妄想科学ADVっていうけど全然科学的じゃなくて悲しい。10年前のテキストゲーをみているよう

風夏

ひたすらだるい、人気絶頂のアイドルと幼馴染で三角関係とか30過ぎたオッサンにはきつい少年誌ファンタジー。そんな簡単にベース覚えたり作曲したりできるわけねえだろ！

ガンダムTHE ORIGIN IV ★

UC最初のモビルスーツ戦のやつ。まあこれはガンダム税なので…

響け！ユーフォニアム2 ★★★

前期は地方予選。全国大会まで行って…部活する女子高生がどんどん成長していくのがよい。

響け！ユーフォニアム ★★★

とにかくみんなかわいい。部活する女子高生の機微がこれでもかと描かれていて（当時理解できなかったのが）つらい。

鉄血のオルフェンズ2期 ★

ガンダム税とられましたって感じ…ラスタルエリオンがそのままってのはどーも納得いかないですね

終末のイゼッタ

なんか考え方が封建っぽい、魔法戦闘のシーンはかっこいいのだけど、幼女戦記を見てしまった今では非常に色あせてみえる。

双星の陰陽師 ★

陰陽師幽霊戦闘、体の一部が人間じゃなくなった変態系の中学生〜高校生の成長モノ。長かった、普通に分かりやすく少年誌でよいはなし。

セイレン

9話までみたけどだる過ぎて切った。ストーリーはともかく作画崩壊が多くて原作の魅力が台無しなのでは。原作みてないけど。

非リアルタイム

dアニメストアで配信された過去の作品を少しずつ見ていく。

Charlotte ★★★

面白くて一気に見てしまった。展開がベタで分かりやすいのだけど、友利がかわいい（そればっかりだけど）のでつい見てしまう。途中で出てきた華僑系っぽいマフィアはえらく中途半端で弱かったり、1年かそこら？で世界中の能力者から能力を奪うなんてできるのか？それだとせいぜい数千人くらいしか能力を奪えない気がするのだけども。

結城友奈は勇者である ★

まあまあいい話だったけど、最後の出来事(大赦が勇者を解放したアレ)だけがどうしてもわからない。女の子に「うおおおおおおおおおおおお！！！！」って言わせるのを楽しむやつ。

未確認で進行形 ★★

日常系なんだけど小紅がとにかくかわいい。前半だるいけど後半からテンポ上がって飽きなくなる。

ソードアート・オンラインII ★

GGO編とエクスカリバー編。詩乃がとにかくかわいいが、展開が1期に比べてちょっと平凡というかスリルに欠ける。スリル要素が少数の悪役に絞られてしまったところが厳しいか。

ソードアート・オンライン ★★

最強主人公モノはやっぱり定番で王道。SAO編はやっぱり命がかかっているというスリルがあって非常によかったが、ALO編はヒールを倒すだけの話になってしまってちょっと残念。あと、2年も寝たきりで意識のない人間はもっとやつれてると思うゾ。

青の祓魔師 ★★

少年誌らしい、飽きさせない展開でつい最後まで観てしまった。

東京喰種√A ★★★

漫画も :re まで全部読んでしまった。喰種という天敵が人間社会に潜伏してるというそのプロットがすでにずるい。登場人物がみんなキャラが立ってて、いくらでも四コマ漫画が書けるみたいだ。

東京喰種トーキョーグール:re 11 (ヤングジャンプコミックス)

東京喰種トーキョーグール:re 11 (ヤングジャンプコミックス)

氷菓 ★★

ウィットに富んだ謎解きの話。しかし高校生にしては教養ありすぎじゃないか？！えるの作画がときどき「あざといなー」と思いながらもついつい見てしまった。

劇場版トリニティセブン -悠久図書館と錬金術少女-（全1話）

トリニティセブン ★

ラッキースケベ学園ハーレム異世界転生もの。敵役との妙な馴れ合いとか、モブの命が軽すぎるとかいろいろ感情移入しにくい要素があった。

東のエデン劇場版 Paradise Lost

記憶を取り戻して母親を探したり。ラストは納得行かない展開だけど、Juisだけはかわいい。100億円使って日本をよくするという話、ニーチェ的な超人論に持ち込んでいて既視感満載だったのでちょっと楽しめなかった。いやそんなに単純じゃねーから…というのは野暮。

東のエデン劇場版 The King of Eden

記憶をなくしてリセットされたところから。ニューヨーク編

東のエデン

巷で言われてるほど…って感じだった。アニメで完結せず劇場版に続く

完走できず

フレームアームズ・ガール

だるいやつ

sin 七つの大罪

魔導学園HxH枠。マリアが可愛くてみていたが、巨乳はそんなに好きじゃないしHxH以上にストーリー皆無だった。

ガリレイドンナ

時間切れ。ガリレイの秘密はまあよいが、それにしても科学まわりのファンタジープロットがいささかお粗末。

BanG Dream!

切った。アニメは最高につまらなかったがゲームが出て売れていると聞いて、ああ俺はお呼びではなかったのかと得心した。

グラスリップ

PAworksということで期待しながら半年くらいかけて少しずつみていたがついに断念(2017/6/7)。岡田麿里路線を目指してみたようが狂気とインパクトに欠ける。

P言語の素晴らしさについて

先週Microsoft社がP言語に関するブログ記事を公開し一部界隈で話題となった。

「いまさら一文字言語かよ…」「何個目だ？」といった批判的諦念的なものから、「RustとGoとErlangの間の子みたいなのだなあ」「なんか読みにくい」といった反応が多くこの言語の重要性やインパクトに対して正しく理解しているものがあまりなかった。尊敬しているTD勢ですらあまり重要性が伝わってないようだ 1 2 。上記のブログ記事を読んだり、マニュアルを読んだらすぐ分かるようなことではあるが、日本語で解説しておこうと思う。なおいわゆる言語入門とかそういった類のものではないことをご理解いただきたい。

TL;DR

  • 並行処理や分散システムの形式証明や形式検証はそれ自体が非常に難しいことが知られていた
  • 証明や検証のツールも、実装のフレームワークも、テストのツールもあったが、形式検証と実装を同時に記述することはできなかった
  • 並行処理や分散システムのプログラムについて、形式検証と実装を同時にできるようになったのがP言語

これを読んですごさが分からなかった人は私のスライドを見てからここに戻ってくるとすごさが伝わるかも。

並行処理や分散システムの正しさを保証するのはとても難しい

そもそも人類にはマルチスレッドが早すぎたのであって、マルチスレッドプログラミングなんてものは常人がやるべきではない類のものであることは一般に知られているといっていいだろう。しかしながらCPUのクロック数IPCは頭打ちになりムーアの法則は演算コアを増やすという方向に進みつつあり、マルチスレッドプログラミング（並行処理）は、夏休みの宿題の終わっていない小中学生に対する9月1日のように差し迫ってきている。

CAS命令などの同期プリミティブが用意されている並行処理でさえその難しさが知られており、いわんや故障の含まれる分散システムをや。FLP不可能性やCAP定理といった「できない」尽くしの世界で、それでも人類はOSを発明し、RDBMSを発明し、非同期IOで動作するHTTPサーバーで日々ネットサーフィンを行い、Hadoopでビッグデータを処理してきたのである。これらのソフトウェアに人類が一体どれだけのリソースを投入し、非決定論的に発生する並行バグのせいでいったいどれだけの時間と機会を失っただろうか。

手続き型のプログラミングでの正しさの保証は実践的にはまだ難しいとはいえ、多くの技術が普及しようとしている。いわゆる型推論に基づいたコンパイル時の型検査と静的リンクの強制（Haskell, OCaml）や、カリー＝ハワードの同型対応を用いたプログラムの形式証明があればプログラムが正しいことを理論的に保証することができるようになった。言語仕様や処理系の実装からそういった形式証明をつけにくいプログラミング言語でも、QuickCheckを始めとしたテストパターンの網羅的な生成とエラーケースの推定をやってくれる強力なツールが登場（普及…？）している。日本語だとxuweiさんのScalaCheckの資料が非常によくできていて分かりやすい。

一方で並行処理や分散システムの正しさの保証は難しい。実装面からのテストツールはしばらく決定版がなかったが2013年のJepsenの登場によって状況は変わった。JepsenはいわゆるFault Injectionと言われる類のテストツールで、特にiptablesを操作してネットワーク分断をシミュレートするものであった。Jepsenによって Kafka, MongoDB, ElasticSearch といった多くの分散システムにバグが見つかり、それから分散システムはJepsenのテストを通ることが登竜門のようになった。ちなみにOverview of Infrastructure TestingというGoogleの記事を見てると、Googleは21世紀のかなり早い段階でネットワーク分断のFault Injectionもやっていたのだろうと推測される。実用的で著名なFault InjectionのツールとしてはChaos Monkeyがかなり早くから知られていたが、これはサービス全体に対する大規模なものであって、特定のソフトウェアを試すようなものではなかった。

他方では、分散システムのアルゴリズム（プロトコル）を形式的に証明して正しさを保証しようという試みはそのもっと昔からあった。上記のMSのブログにあるTLA+とSPINモデルチェッカが代表的なものだ。しかしこれらはいずれも、アルゴリズムを検証するために独自言語が必要であり、実用的なものではなかった。具体的には、これを使ってアルゴリズムが正しいことを証明できても、実際に動作するソフトウェアは別の実用的な汎用言語（CやJavaなど）で記述する必要があり、プログラムが証明された通りに実装されていることを保証する方法はなかった。ちなみに形式記述とFault Injectionの間の子としては最近、MollyがNetflixで実用化されたことが話題になった。Mollyは Dedalus というDSLで記述したアルゴリズムに形式的にFault Injectionを網羅的に仕掛けてバグを出すものである。わたしは上のブログ記事で埋め込まれているPeter Alvaro のRICONでの講演を見ることができたが、これは本当に面白かった。トップレベルの研究者は話も上手くないといけない。

少し話を戻して、並行処理のプログラム（いわゆるマルチスレッドで動作するプログラム）の正しさを検証する方法で私が一番良く知っているのはErlangのQuickCheckが持っているPULSEだ。これは相互作用する2つのFSMを並べて状態とメッセージの組み合わせを網羅的に試してRaceが起きる条件を絞り出していくというものだ。他にも eqc_statemなど素晴らしいツールがあるので、ErlangやElixir使いでRace conditionに悩んでいる諸君がいたら是非使うべきだ。決して値段は安くはならしいが、本番で競合で悩むくらいならこれをサクッと買った方がよい。Erlang以外の処理系でここまで踏み込んだものはあまり知らない。もっともそこまで必要ないという話かもしれないが…　他の言語なり処理系だと、GoのRace detectorやClangのThread Sanitizerくらいが有名だろうか。僕も詳しくないので教えてほしい。まあDTraceやBPF, ClangのXRayを使えばどうにでもなるという話かもしれないが、どのツールも私のような凡人に無理じゃないかと思う。

おわかりだろうか。これだけ日進月歩で研究と実践の歴史が積み重ねられてなお、 1) 分散システムや並行処理を形式検証するDSL, 2) Fault Injectionしてみて動くかどうか確かめてみるテストフレームワーク, 3) とりあえずトレース仕掛けてじっと様子を睨む といった方法くらいしかないのである。ここに颯爽とP言語が登場するのである。

P言語そのものについて

実はP言語は先々週登場したわけではなく、2012年には存在が公表され、2013年にはPLDIに論文が登場した。さらに昨年10月にはソースコードが公開された。余談だが、実は遅くとも2014年にはCodePlexでコードが公開されており、たとえば "a1cd6fa" は完全に一致している: Codeplex, GitHub。じゃあ一体このInfoQの記事は何だったのか。このInfoQではP言語で書いたコードをZingという謎システムに入れて検証できるようにしたと書いてある。今年の記事では、P言語からC#の形式検証用のコードを吐いてツールに食わせることができると書いてある。2012年からいろいろあったんだね…

P言語のどこがすごいかというと、P言語でシステムを書くと、本番で動作する分散システムのC言語でのプログラムと、形式検証ツールに食わせるためのC#のプログラムが同時に生成されるのである。このP言語のコンパイラツールチェインが正しく作られている限りにおいては、形式検証済みの分散システムを本番で使うことができるのである。理論的にはバグがないというやつである。ネットワーク分断も死んだふり故障も（もしかしたら、書き方によってはビザンチン故障も）もう恐れなくてよいのである。TLA+は僕にはちょっと難しいのだけど、僕がもし次に分散システムを手作りする必要があったら、まず最初にP言語での実装を検討するだろう。なのでまずはMacPortsで使えるようになってくｒ（軟弱

ここまで来ると、Rust的なメモリ管理とか、Go的な軽量プロセスや、Erlang的な状態遷移マシンの記述なんていうのはモダンなシステム実装言語にはあって当たり前で、そこからもう一歩進んで何があるかが決め手になるということが分かる（もちろんRustやGoが劣っているということではなく、他によいところがある）。

ちなみに、この手のものは実はP言語とは違うMicrosoftの別チームが同様のものを出している。その名もIronFleet だ（よくわからない日本語解説、よくわかる解説）。カタログスペックのコンセプトは、実は全く同じだ。何だか強そう。著者の名前を見比べるとわかるが、P言語とは全く別のチームだ。キャンパスが違うんだろうか、仲はいいのか悪いのか、実績からいうとP言語の方が強そうだよなとか、いろいろ妄想できてなんか楽しい^^;

レポジトリをもうちょっとうろうろすると、入門PPTがなんとそのまま入っていて(ﾉ∀`)ｱﾁｬｰと思ったがその内容が思ったよりすごい。なんとHololensやOfficeでも使われているというのだ。実績も十分だ。こんなすごい言語が使われているAzureやWindowsを使ってみたくなるね^^;

f:id:kuenishi:20170525081934p:plain

参考

P.S. とりあえずMacOSでの最初のビルドは見事にコケた。Sierra 10.12.5, commit 601520c8, monoとcmakeはMacPortsから。
P.S. mono >= 4.5 が必要だと id:matarillo さんにブコメで教えてもらった。
P.S. コメントで本文は形式的証明と形式検証を混同していることを指摘していただいた。その辺りは割り引いて理解していただけると助かる。
P.S. プログラムと検証を一致させる試みは何もPやIronFleetが初めてなわけではなく先行者がいることもコメントで指摘いただいた。割り引いて読んでくれ。
P.S. TD勢に対する煽りが少し攻撃的だったのでマイルドな表現に修正した。

一次情報を確認しなければ信頼性のある記事にはならない

こんばんは、やっと先週ガノンの打倒という宿願を果たし、ハイカラシティからもいささか足が遠のいてしまった私であるが、なんとか季節の変わり目にも風邪を引かずに過ごせている。読者諸賢はいかがお過ごしだろうか。はや4ヶ月、1年の1/3が過ぎてしまったが、先日の大🔥炎🔥上🔥騒🔥ぎで2017年のクラウドを何だか占い損ねた件を覚えておられるだろうか。これが公共のメディアに書く価値があるどころか、記事で取り上げられた会社の名誉や主張を歪曲しかねないものであったことを。

本日、友人に教えられ、同じ記者が同様に見過ごせない記事を書いたことを知ったので、いっそ皿まで、いやとりあえず再度批評することとしたい。それがこれである。リンクを踏んでPVに貢献することは結構だが、後悔するのでやめておいた方がよい。

it.impressbm.co.jp

リンク先を読んでない方は、次の指摘からもおおよそのクオリティがおわかりいただけるだろう。

この平氏を直接は私は存じ上げないが、Redhat Linuxに非常に精通しており、恵比寿でコンピュータ・ソフトウェアに関する仕事をしているということは事実のようだ。

AWSとの戦略的提携を発表、OpenShift Container PlatformからAmazon Redshift、Amazon AuroraなどAWSのマネージドサービスがダイレクトに利用可能に

これが平氏の指摘であるが、AWSとRedhatはもともと戦略的提携をしており、双方の公式発表をみても　Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift , Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift と、いずれも "Extend Strategic Alliance" という表現を使っている。これは、素直に英語を読めば「もともと戦略的提携をしていたが、提携を拡大しOpenShiftからAWSを使えるようになった」という話になる。まったく提携していなかった2社が提携を始めるわけではないので、これではニュースバリューを偽って誇張している表現である。

これまでどのような提携をしていたかは、Redhatが出しているフォローアップの記事 AWS and Red Hat -- Digging a little deeper を見ればすぐに分かる。本文の早い時点で "March 2010 was an exciting month in the collaboration history of Red Hat" （2010年3月はRedhatの歴史上とてもエキサイティングな月だった）と書かれており、ここからAWSとRedhatの提携が始まったことがわかる。具体的にはEC2のMarketPlaceでRedhatのサブスクリプションつきのイメージが買えるようになったのだと記憶している。こちらの記事 - AWS Partner SA ブログ: AWS上のRHELのサポート体制とアップデートサーバー は2015年であるが、その内容がわかりやすく日本語で書かれている。また、今回の提携拡大の伏線としては Deploy Red Hat OpenShift on Amazon Web Services | AWS Partner Network (APN) Blog が分かりやすい。AWSが大好きな顧客の声を汲むなら、「ここまで来てるんならもういっそAWS隠蔽して適当に使えるようにしてくれよ！」だろう。

次はこちらだ。

コンテナベースでクラウドネイティブなアプリケーション開発環境「Red Hat OpenShift.io」を開発者向けに無償提供

OpenShift.io The Gathering – Summit 2017 – Developer Tools, Overview and Roadmap Part I には、

OpenShift.io is the next generation OpenShift platform, based on OpenShift 3, for building and running applications in the cloud.

と書かれている。ここで重要なのは "building and running applications" という部分で、正確に訳すなら「アプリケーションの開発と実行」である。つまり、OpenShift platformはアプリケーションの開発環境と実行環境を兼ね備えたものであり、開発環境だけのものではない。この記事を丁寧に読んでいけば、OpenShift（コンテナのオーケストレーション技術）がどのようなものかはすぐに分かるだろう ( 新野さんの記事も非常に分かりやすい )。2017年のクラウドを占ったときの「これからはDevOpsがクラウドで重要になる」というフワッとした指摘を奇しくも裏付けた形になり、それをベースに記述を肉付けしたら伏線を拾ったもっとよい記事になったであろうに、勿体ない。

Disney、Pixarなどのユースケースに見るOpenStackおよびコンテナ関連のビジネスの拡張

これは、どうしてこういう表現になるのか分からない。残念ながら私も現地には行っていないので分からないが、おそらく Disney Studios and Pixar use OpenShift to accelerate the delivery of platforms and services のセッションを指しているのだろうと思うが、少なくともOpenStackという文字は文中になく、むしろOpenShift推しなのが分かるだろう。また、セッションの検索 をしてみても、OpenStackは32件、OpenShiftは95件のセッションがマッチした。これをみても分かるようにOpenStackは下火で、OpenShiftとコンテナオーケストレータの採用が拡大している傾向の方がニュースとしては正確である。ひょっとしてOpenShiftとコンテナとOpenStackの関係が理解されていないのでは…とうっかり疑ってしまうので、その関係がよく整理されている OpenStack、Docker、OpenShiftの関係を理解する！ レッドハット朝活セミナーのご紹介 | RED HAT OPENEYE を紹介しておこう。

そして、推測にみちたこの文章

今回、その距離を一気に縮める提携を発表したことは、AWSと近しい関係を構築するほうがメリットが大きいと判断したといえる。

は、「ただのパートナー→戦略的提携」という前提にもとづいているが、もともと戦略的提携していたのだからこの文章はほとんど意味がない。私の考えでは、今回のサミットで特に距離を縮めたということは別になくて、その傍証として、キーノートにAWSからの有名人（例えばWerner VogelsやHamilton）どころか、誰もキーノートで話していないことを挙げておこう。しかも、セッションスピーカーで検索してもAWSのスピーカーが3人しか見つからなかったことも付け加えておこう。

で、「プライベートクラウドとパブリッククラウドの境界線がより曖昧になっている流れ」とは一体何なのか。ハイブリッドクラウドのユースケースが増えていることを指すのだろうか。境界線が曖昧とは一体どういう意味なのだろうか。少なくともシステムの管理主体と利用者がはっきりしている限りは境界線が明確にあると思うのだが、考えれば考えるほど意味がわからない。

次は「エンタープライズ企業によるDockerの採用が増えるにしたがい、オープンソースコミュニティを重視するスタイルをビジネスと両立させることが難しくなってきたのも事実だ」という表現だ。何が難しいのだろうか。私は仕事で体感したから知っているが、難しい理由は具体的にはモノによって様々に異なっており一般論として述べるにはまだ十分早いと思う。なぜなら直後に記事でべた褒めしているRedhatがサブスクリプションモデルで成功しているからだ。

いちおうDocker CEO 退任の挨拶から以下の文を引用しておこう。

Docker has the potential to become not only one of the most enduring technology companies, but also a transformational platform, technology, and movement; I can’t think of a better or more qualified individual to lead us to that future than Steve.

オープンソースソフトウェアでビジネスをするのは難しいということであるが、さてここでCrunchBaseのランキングを指摘しておこう。この記事で取り上げた Docker (26位) よりも Hortonworks (152位) よりも、第2のRedhatに近い存在がいる。 "Open Source" "Enterprise Software" でカテゴリを any 検索するとすぐに出てくる、12位の、先日IPOしたヤツである。

f:id:kuenishi:20170509235744p:plain

まあこのランキング、IPOしてるしてないとかゴッチャだしRedhatは登場しないし、IBMがかなりの下位だったりと独自のランキング手法であるが、今調べたら時価総額で3.5倍程度差がついているこの会社をスルーしてHortonworksを取り上げるのは数字上はかなりアンフェアだと私は思う。ちなみに、150位くらいまでに出てくるOSS企業は MongoDB (56位), Pivotal (128位), Elastic (168位), Databricks (182位), あたりがある。

Windowsで作ったzipファイルをMacで展開するとファイル名が文字化けする問題

日本の商習慣として未だに残っているのが「ファイルをまとめてzipで渡す」というやつである。数年前までビジネスで使われるコンピュータはWindowsがデファクトスタンダードだったので、zipファイルを作成するのも、展開するのも同じソフトウェアを使っていたから特に問題が起きることはなかった。古き良き時代であるが、近年ではMacOSも普及し、ビジネスでファイルをやりとりするのに使えるようになってきた。複数のOSが併用されるようになったが、相変わらずファイルのやりとりはzipで行われるという商習慣の形として残った。

私の意見はそもそもそういう商習慣を撤廃するべきだということに尽きるのだが、家族を養う手前既存の商習慣に従わなければならない。そしてここ数年は、仕事でもMacOSを使っている。MacOSとWindowsの間でファイルをやり取りするときの問題その1は暗号化zipである。問題その2は表題にあるとおり、日本語のファイル名を持つファイルが文字化けしてしまい、意味のあるファイル名だったときにビジネス上のコミュニケーションに支障が出てしまうことである。

もしビジネスでなかったらそんなファイルはすぐにrmしてしまうべきであるが、ここまで読んで頂いたということは、読者諸賢もこの問題でお困りのことであろうから、私の調べたことがいくらかでもお役に立てば幸いである。

TL;DR

なぜファイル名が文字化けするのか

Windowsのファイルシステムでは、基本的に日本語のファイル名はcp932でエンコードされている。後方互換姓のためこれが今後も変わることはないと思われる。また、最新のWindowsでもUTF-8などでファイル名をエンコードしてzipアーカイブを作ることはできないようだ。Explororのメニューからアーカイブを作るとcp932でファイル名もzipアーカイブ内に保存されてしまう。7zipなどのサードパーティのアプリケーションを使えば、Unicodeでアーカイブすることができる。

また、ZIPの仕様では、ファイル名のエンコーディングに関する指定はAppendix Dに 「歴史的にIBMコードページ437しかサポートしていなかった」と書かれている。CP437とは何かというと、いわゆるASCIIのセットにラテン文字を追加したもののようで、当然日本語の文字が入っているわけではない。CP437はDOSのOEMコードセットというらしい。ここでいうDOSはMS DOSのことであるから、WindowsにIBMコードページが追加されていき、日本語版Windowsのファイルシステムの標準文字コードとして、また、そこから作られるZIPアーカイブでCP932が採用されることのは歴史的な経緯としては自然なようだ。

一方、MacOSのファイルシステムは、 APFS でも HFS+ では、基本的にUTF-8でファイル名がエンコードされている。

APFS has case-sensitive and case-insensitive variants. The case-insensitive variant of APFS is normalization-preserving, but not normalization-sensitive. The case-sensitive variant of APFS is both normalization-preserving and normalization-sensitive. Filenames in APFS are encoded in UTF-8 and aren’t normalized.

HFS+, by comparison, is not normalization-preserving. Filenames in HFS+ are normalized according to Unicode 3.2 Normalization Form D, excluding substituting characters in the ranges U+2000–U+2FFF, U+F900–U+FAFF, and U+2F800–U+2FAFF.

Finderのメニューで展開しても、 `/usr/bin/unzip` を利用しても、基本的には zip アーカイブ内のファイル名のところにあるバイト列をそのままファイル名として展開する。したがって、UTF-8しか対応していないHFS+のファイル名に、CP932でエンコードされた文字列が保存されてしまう。Finderを始めとした各種アプリケーションはHFS+の仕様に従ってUTF-8だと思ってCP932のファイル名を表示するので、よくわからない化けたファイル名が表示されることになる。
　
まとめると、WindowsではCP932でZIPを作る、ZIPは慣習的にCP932やCPxxxでのファイル名のエンコードを許容している、MacOSはそんなことしらないでUTF-8として扱う、のコンボで、結果的にこういうことになるようだ。

f:id:kuenishi:20170508224724p:plain

ワークアラウンド、今後の期待

Macに含まれているInfo-ZIPが6.00であるから、それが最新版にアップデートされれば解決するか？という答えは半分正解で、半分不正解だ。まず、このCP932対応が含まれているバージョンがまだ正式にリリースされておらず、ベータ版が 2010年にリリースされて以来ずっと放置されている。どうもやる気がないないらしい。スレも立っているがやはり放置されているので期待できない。こんなに必要とされているソフトウェアなのにリリースされないとは、OSSはさすがにかくあるべしといった感がある。

もし万が一これがリリースされたとして、MacPortsに入るのは早いだろうが、MacOSのリリースにバンドルされるのはいつのことになるやら知れたものではない。現にPythonは2.7だし、Rubyだって今みたら未だに2.0.0である。

つまり公式は期待できないので、ZIPファイルを受け取るMacOS側がどうするべきかというと、

くらいが関の山である。

次点で期待できるものとして、Goで書かれた mholt/archiver にパッチを当てるというものがある。 x/text/encoding/japanese を使うとよさそう。有志に期待している。もしGoを書きたくなったら僕がやるかもしれない。

ZIPアーカイブを作る側、Windows側でできることがあるとすれば、 UTF-8 によるエンコードはサポートされていないようなので、もし相手がMacユーザーだと分かっている場合は、予め 7zip 等のサードパーティツールを使ってUTF-8でZIPアーカイブを作成するのがよさそうである。

おまけ、問題3、逆: Macで作ったzipアーカイブが中に日本語のファイル名を持つときにWindowsでファイル名を文字化けさせずに展開できるか

UTF-8のファイル名が保存されたものは Windows 7のあるバージョンからできるようになっている。これは、ZIPの仕様に、ファイル名がUTF-8でエンコードされていることを示すフラグがあり、それに従ってファイル名を変換しているようだ。

   4.4.4 general purpose bit flag: (2 bytes)
   ...(snip)...
        Bit 11: Language encoding flag (EFS).  If this bit is set,
                the filename and comment fields for this file
                MUST be encoded using UTF-8. (see APPENDIX D)


しかしながら、 MacOS のFinderでのアーカイバはそのフラグをつけずに UTF-8 でエンコードしてしまうらしい。

一方MacOSに含まれている "/usr/bin/zip" コマンドは Info-ZIP の 3.0 なので問題はなさそうだ *1 。リリースノートに "Unicode (UTF-8) filename and (partial) comment support" と書かれている。

参考

File and folder names on HFS Plus consist of up to 255 Unicode characters with a preceding 16-bit length, defined by the type HFSUniStr255.

*1:Finderはこのツールを使っていないということか…？！

最近のトレ

もともと健康のために始めたトレーニングだが、なんというか一区切りついたのでここに記録しておこうと思う。いろいろな記述があるが全て個人の感想であり科学的根拠はないので眉に唾をつけて読んでいただきたい。

目標

健康診断で脂肪肝と診断され体脂肪率が23%まで増え、体重は 75kg くらいまで増加した。全く運動をする機会はなく、しかも週のほとんどを在宅勤務にしており、息子を朝幼稚園に送っていく（徒歩１分）のみ、という危機的な状況であった。

一年発起してジムに通い水泳や筋力トレーニング、有酸素などをやってみるも水泳と有酸素はなかなか景色が変わらず飽きやすかった。筋力トレーニングは集中力が重要な一発勝負で好みに合っていたので続けることにした。その際いくつか目標を立てた。

メニュー

コンディショニングは 2016年のまとめ - kuenishi's blog に書いたとおりだ。いまの会社は遠方なので仕事後にジムに行くのは少し気力が必要だったので基本的には土日のどちらか週１回しか行っていない。余裕があるときは帰宅後夜遅くの週２になる。週１回なので基本的には毎回同じメニューをこなす。メニューはビッグ３を中心に

  • チンニング
  • ベンチプレス
  • フルデッドリフト
  • ケーブルプレスダウン
  • ローロー
  • ラットプルダウン
  • ドラゴンフラッグ
  • レッグエクステンション
  • ダンベルリストカール
  • ダンベルベントオーバーローイング
  • レッグプレス

などから数種目、気が向いたものをこなす。余裕があればまれに新しい種目も挑戦する。ビッグ3は定期的にYouTubeの動画でいろんな人のフォームを勉強する。このうちチンニング、ベンチプレス、デッドリフトはリストラップをつけてやる。チンニングは手首や肩の保護が目的だが、ベンチプレスやデッドリフトはパワーアップに多少貢献している（気がする）ので使っている。Schiekの24インチのものを使っている。締め付けは十分だが、やはり手首の保護となるともう少し長いやつがほしい気もするが、概ね満足している。アフィリエイト:

Schiek シーク リストラップ 24インチ ブラック フリーウェイトトレーニング用 (国内正規品)

Schiek シーク リストラップ 24インチ ブラック フリーウェイトトレーニング用 (国内正規品)

トレ前は時間の余裕次第だが、マッサージチェア、ストレッチポール（Pole）、ストレッチボール（Ball）を使って背中と肩を中心に15分程度コンディショニングする。下半身も基本的なストレッチをしておく。

トレ後は特に何もしない。シャワーを浴びて帰るか、帰ってシャワーを浴びるかだ。

肩がまだ状態がよくないのでチンニングはパラチンか逆手が多い。順手はまだ手首に負荷がかかる気がしているので少なめだ。Yチンは背筋がまだ弱くて十分に上がらない。

ベンチプレスはロシア式?の 5x5 をやっている ( 伝統の8×2と高頻度トレーニング、5×5ルーティンの解説 | SBD Apparel Japan コラム , パワーフォームを導入した「ベンチプレスを強くするためのトレーニング」（3/4） ) 。5x5 は5repまわしたらすぐ重量を増やすのでルーティンに入りやすい、完全にバーをコントロールすることが増量の条件、始めは軽いのでアップ少なめでも始めやすいので結局時間の節約になる、等々メリットが多く、普通の6~8rep x3set のものよりも私に合っているように感じる。

デッドリフトはビッグ3の中でも最も難しい種目のはずなので、重量や効果よりもフォームを意識している。これは始めてまだ2ヶ月程度なので、背中と腰が常に伸びた状態を維持することを心がけている。むしろ少し尻を出して反らせるくらいのイメージ。背中を伸ばしたまま地面をゆっくり押して、最後に体をまっすぐにする。背中が少しでも曲がると腰に負担がかかって怪我のリスクが増大することを実感しているので、慎重に継続していきたい。フルデッドリフトやるときは体の柔軟性も重要なので、ストレッチはまめにやっておこうと心がけている。

他のメニューは主に背中と腹の基本的な筋肉を広めにカバーするようにしている。

レッグプレスはまあ、一番大きい筋肉を鍛えてテストステロンを増やしたいのでやっている。これが一番きついので基本的には最後にやる。

ジムに行けないとき

どうしても諸々が積み重なってジムに行けないときは上記のようなハードめのメニューがこなせない。それで2週間とか開いてしまうとかなりつらいので、もらいもののパワーブロックで2,3日に一度なるべく家でトレーニングするようにしている。これ（アフィリエイト）は新型のもの：

【正規品】POWER BLOCK（パワーブロック）アドバンスタイプ SP50　［50ポンド/23kg］

【正規品】POWER BLOCK（パワーブロック）アドバンスタイプ SP50　［50ポンド/23kg］

だが、僕は1世代前のものを使っている。普通のトレーニーなら23kg程度はすぐに軽くなってしまうので、できれば90ポンド(~41kg) asin:B0029NHOMI のものを買っておくのがよいだろう。これと椅子を適当に組み合わせて

  • プッシュアップ、プランク
  • ダンベルアームカール
  • ダンベルショルダープレス
  • ブルガリアンスクワット
  • ダンベルベンチプレス

などを（ごくまれに）やっている。ダンベルベンチプレスが特に面白くて、ストレッチポールを縦にして背中〜腰を乗せてダンベルを押すと左右のバランス感覚も同時に鍛えることができるので面白い種目になる。床の上でやるとどうしても可動域が小さくなってしまうが、そこはまあ仕方がない。ストレッチポールを何か厚めのマットの上に乗せてやるとよいかもしれない。

口に入れるもの

食事は妻が作るものに合わせる。要望を聞いてくれるので、ブロッコリーや脂肪の少ない肉を中心に作ってもらうことが多い。自分のための外食は極力避けるようにしているが、妻に負担をかけないとか友人との付き合いの場合は外食も厭わない…とはいえなるべく高タンパク低脂肪の店を選ぶようにしている。

朝夕にエランバイタルを１錠とプロテインを飲んでいる。エランバイタルは本当は一回6錠なのだがちょっときついので1錠だけにしている。エランバイタルを飲むようになってから翌日の疲労感が少なくなった。プロテインは学生時代から使っているこれ（アフィリエイト）:

ウイダー マッスルフィット プロテイン バニラ味 2.5kg

ウイダー マッスルフィット プロテイン バニラ味 2.5kg

を、低脂肪乳と水の1:1の混合液に溶かして飲んでいる。なぜ混合するかというと、水だけでは味が残念だし、牛乳だけでは余計な脂肪を取りすぎてしまう（気がする）からだ。まあ私程度の雑魚ではどっちにしてもあまり変わらない。

トレーニング前は特になにも摂らない。トレーニング中にCCDを700cc程度摂って血糖値を下げ切らないようにしている（アフィリエイト）。

グリコ パワープロダクション CCD エネルギー&水分補給 ハイポトニック粉末ドリンク 大袋 10リットル用 900g

グリコ パワープロダクション CCD エネルギー&水分補給 ハイポトニック粉末ドリンク 大袋 10リットル用 900g

CCDの代わりにスポーツ飲料や茶を飲むことはない。そういった飲料では血糖値が下がりきってしまい1時間弱で集中力が切れてしまうからだ。CCDがあればそんなことは起きない。気合を入れてハードにやる覚悟をしたときはこれにBCAAを5~10g添加する。

ゴールドジム BCAA アルギニンパウダー 400g [その他]

ゴールドジム BCAA アルギニンパウダー 400g [その他]

BCAAはトレ中のCCDに混ぜるか、トレーニングした日の夜のプロテインに必ず入れることにしている。BCAAがあると筋肉の疲労がとれやすい。

トレーニング直後30分程度の時間をゴールデンタイムといって、プロテインの摂取が最も効果的だと言われている。しかし私は朝夕のプロテインだけにして、トレーニング直後に何か摂取することはしていない。理由は

  • そもそもCCDを飲みまくって腹がふくれているので、追加で入らない
  • BCAAのようなアミノ酸ならともかく、内臓での消化吸収に数時間〜数十時間はかかるので結局アミノ酸が細胞に到達して合成に使われる時間はもっと後なのでそんなにタイミングは重要ではない
  • ジムに持っていくのはかさばって邪魔

といったところだ。特に科学的根拠があって結論しているわけではないので、反論は聞きたいところ。

脂肪はなるべく摂らない。できれば量を毎日測定する。脂肪はなるべく摂るべきではないという話には異論があって、脂肪酸は細胞膜の合成などにも使われるので人体には必須の栄養素だ。だから融点のなるべく低い（なるべく酸化していない）脂質を中心に最低限の量は毎日摂るべきだと思う。ただし僕はそこまで食事をコントロールできていないので単に「肉の白い部分や、液体の油を使った料理はなるべく摂らない」という運用にしている。

炭水化物は、特に制限していない。本当は基礎代謝から一日の摂取量を算出すべきだが、これも私はあまり我慢せずに食べることにしている。なぜなら、私は空腹になると体全体が倦怠感に覆われてしまって能力が大幅に落ちてしまうからだ。知能も低下する。これは血糖値の低下が原因だと思われるが、おそらくその際に体内の筋肉を分解してエネルギーに変換していると思われる。これではトレーニングした意味がないので、朝昼夕は炭水化物と蛋白質をなるべく均等量摂るようにしている。それでも昼食と夜の間は時間が開いてしまうので、オニギリなどを食べて血糖値を下げないようにしている。夕食が早かった場合は寝る前に空腹になるので、夕食を多めに摂るか夜食を摂ることにしている。あえて気をつけているのは、アミロペクチン系のものよりもアミロース系のデンプンが多いものを選ぶようにしているくらいか。後者の方が血糖値が上がりにくい（＝持続しやすい）らしい。

カーボを恐れるな。

モチベーションの維持

これが一番難しい。基本的には「重い物を持ち上げるのは楽しいことだ」と繰り返すのがよいのだが、自助努力だけでは限界があるので、いくつか組み合わせている。

  • 雑誌（アイアンマン）を毎月購入、読めなくても見えるところに積む
  • 毎日プッシュアップくらいはやる（コンディションの低下を早めに検知してトレーニングの心理的優先度を上げる）
  • 定期的にムービング・ターゲット moriyoshi や ymotongpoo に会って自らの肉体を恥じる。

特にアイアンマンの購読はよい。毎月いろんな人のいろんな技術があるので試してみたくなるし、いろんな写真を見てふと足元を見ると「はー」という気持ちになれる。

アイアンマン2017年4月号

アイアンマン2017年4月号

結果

久しぶりに会う人に「肩が厚くなったね」と言われることが増えた。腹はそんなに変わっていない。太股は太くなった。ジーンズは腰回りを2サイズ落とした。子供を抱っこできる持久時間が少しだけ長くなった。

ベンチプレスの結果に注目いただきたい。ついに自重を超えたのである。体重は一度70kgを切った（その後減量をやめてパワーアップに振った）ので、目標 2/4 を達成したことになる。ベンチプレスは100kgまではすぐに誰でも上げられるようになるそうだが、私のような軟弱エンジョイ勢でも週一回続けていればここまで来れることが分かった。感覚としては5x5とコンディショニングが効いてるなと思う。

近所にゴールドジムがほしいなぁ…

こういうの本当にやめていただきたい

anime

f:id:kuenishi:20170215024411p:plain

いやまあこれなんだけど。昨日急に通知があったということは計画停止じゃないというわけで、そんな前日にダウンロードしてくださいませ！とか言われてもできるわけねえだろ！ダウンロードするくれえなら見るわ！



過去もだいたいこの時間。


たとえば検索すると「重要なお知らせ」が引っかかるんだけど…この時間に止めるということはこの時間が一番トラフィック少ないわけで、みんな割と昼間とか朝観てるの…まじで…っていう感じです。

こんなにメンテナンスばかりしていて本当に大丈夫なの、システムちゃんと作れているのかとても心配、というか、まあ安いから入ってるんだけど、こういう感じで何もアナウンスなくメンテナンス入られるんならまた移行考えちゃうYo...