読者です 読者をやめる 読者になる 読者になる

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の間の子としては最近、MollyNetflixで実用化されたことが話題になった。Mollyは Dedalus というDSLで記述したアルゴリズムに形式的にFault Injectionを網羅的に仕掛けてバグを出すものである。わたしは上のブログ記事で埋め込まれているPeter Alvaro のRICONでの講演を見ることができたが、これは本当に面白かった。トップレベルの研究者は話も上手くないといけない。

少し話を戻して、並行処理のプログラム(いわゆるマルチスレッドで動作するプログラム)の正しさを検証する方法で私が一番良く知っているのはErlangのQuickCheckが持っているPULSEだ。これは相互作用する2つのFSMを並べて状態とメッセージの組み合わせを網羅的に試してRaceが起きる条件を絞り出していくというものだ。他にも eqc_statemなど素晴らしいツールがあるので、ErlangやElixir使いでRace conditionに悩んでいる諸君がいたら是非使うべきだ。決して値段は安くはならしいが、本番で競合で悩むくらいならこれをサクッと買った方がよい。Erlang以外の処理系でここまで踏み込んだものはあまり知らない。もっともそこまで必要ないという話かもしれないが… 他の言語なり処理系だと、GoのRace detectorClangの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で使えるようになってくr(軟弱

ここまで来ると、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のマネージドサービスがダイレクトに利用可能に

これが平氏の指摘であるが、AWSRedhatはもともと戦略的提携をしており、双方の公式発表をみても 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の歴史上とてもエキサイティングな月だった)と書かれており、ここからAWSRedhatの提携が始まったことがわかる。具体的には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を使っている。MacOSWindowsの間でファイルをやり取りするときの問題その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はDOSOEMコードセットというらしい。ここでいうDOSはMS DOSのことであるから、WindowsIBMコードページが追加されていき、日本語版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" と書かれている。

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

最近のトレ

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

目標

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

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

メニュー

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

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

などから数種目、気が向いたものをこなす。余裕があればまれに新しい種目も挑戦する。ビッグ3は定期的にYouTubeの動画でいろんな人のフォームを勉強する。このうちチンニング、ベンチプレス、デッドリフトはリストラップをつけてやる。チンニングは手首や肩の保護が目的だが、ベンチプレスやデッドリフトはパワーアップに多少貢献している(気がする)ので使っている。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日に一度なるべく家でトレーニングするようにしている。これ(アフィリエイト)は新型のもの:

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

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

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

口に入れるもの

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

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

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

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

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

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

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とコンディショニングが効いてるなと思う。

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

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

f:id:kuenishi:20170215024411p:plain

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



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


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

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

大根はなぜ消化によいのか

夕食で大根の煮物が出てきた。冬はやはりこういうものに限る。暖まるなあ…消化にもいいらしいし…と思ったところで、ふと大根はなぜ消化によいのだろうか?という疑問がわいた。大根は動物ではないのだから食物を消化する必要はないわけだ、消化酵素というものが含まれているが、酵素は通常は動物の体温程度の方が活性が高いので地面に埋まってる大根が低温で持ってても使う機会ないんでは…?などと疑問は尽きない。

我々取材班は早速Google経由でWikipediaに向かった(夕食を食べてダンベルのメニューとブルガリアンスクワットと、スプラトゥーンのガチマッチを10戦ほどこなした後で)。

f:id:kuenishi:20170211213057j:plain

大根おろし - Wikipediaには「大根にはアミラーゼ、プロテアーゼ、リパーゼなどの消化酵素が豊富に含まれているが、これら酵素は熱に弱いため、加熱をともなう調理法では有効に利用できない」と書かれており、主に三種類の消化酵素が含まれていることが分かる。この三種類の酵素について、調べていこう。

アミラーゼ

アミラーゼは、デンプンを分解する酵素だ。というのはあちこちの料理サイトから、いかがわしい健康ダイエット系のサイトまで、どんなところでも書かれている。過熱すると酵素はこわれちゃいから大根はなるべく生で食べましょう、消化がよいのでダイエットに効果ありますぜ!と、そういうのは無視したいのだけど、もうWebは汚れてしまっていてほしい情報に辿り着くのは非常に難しい。

しかしアミラーゼについては案外簡単に答えがみつかった。ダイコンのアミラーゼ | みんなのひろば | 日本植物生理学会が非常に詳しい。いわく「大根にはほとんどデンプンがないのに、どうしてその消化酵素が多く含まれているのですか?」という非常に鋭い質問だ。しかも実験までされている。最近の塾ってすごいんだな…とにかく、要点を引用すると

  • デンプンはデンプン粒として1〜0.5%存在しているとのことです(澱粉科学35: 19 (1988))
  • ダイコンの根は〜90%が水分であることからすれば、そんなに少ないわけでもありません
  • アミラーゼは植物細胞中で、原形質ではなく成熟細胞の大部分の体積を占める液胞の中に局在
  • デンプン粒は液胞の中ではなく、原形質に存在
  • 相互に接触していないため、デンプン粒がアミラーゼによって分解を受けることはありません
  • 冬大根であれば秋―冬での光合成産物を根に貯え、春に種子ができるときそのエネルギー源として根のデンプンを利用していると考えられます

ということだ。動植物が冬を越すためにエネルギーを蓄え、その中でデンプンと同様にアミラーゼも蓄えられているという精巧な仕組みになっている。ではデンプンの消化を助けるというが効果のほどはどうなのか。唾液や膵液に含まれているアミラーゼの含有量はわからないけど、

から、なんとなくオーダーが推測でき…ない。大根おろしを1リットルほど食べれば補助にはなるかな。食べ過ぎかな。

まとめ

分子生物学とか化学ちゃんと分かってないと説明するのは難しい。あと市井の情報源はほとんど信頼に足らず、どれだけ食べたらどういう定量的効果が得られたのかといったデータを全く語っていない。
タンパクを壊すタンパク・プロテアーゼのような面白いページで時間を溶かしてしまって簡単には目指す知識にたどり着けなかった。人類の膨大な知的資源を投資し続けているだけのことはある。

筑波大学で分散システムの話をしてきました

また呼んでいただいたので、筑波大学の情報システム特別講義D(1/19, 20 - 20日4限)で話してきました。これは業界で川島さんに無茶振りをされた人が聴講に来た大学生を置き去りにして講師陣に実力を試されるという素敵なイベントです。発表に使ったスライドはこちらです。自分で論文読んで証明を考えながら作ったスライドなので曖昧なところや誤りがあれば指摘いただきたいです。

前回はデータベースの話をしました。

kuenishi.hatenadiary.jp

今回は、転職もしたし、NoSQLブーム的なのも一通り終わったのでもうデータベースの話でもねーだろってことで、分散システムの理論面に入門した内容になっています。分散システムの理論面は20世紀に一通り出揃ってしまって、21世紀の最初の15年は実装と運用の時代でした。具体的には、理論と実装のギャップをどう埋めるかという研究や試行錯誤が盛んで、理論それ自体の進歩はそれほどでもなかったと思います。…と言いながら、自然言語で記述する分散システムの証明に限界があって人類には難しすぎるのも事実なので、その検証や証明を補助するツールや理論がいくつか試された時代でもありました。そのあたりは発展編として、私はカバーできませんしませんでしたが、10年後には現場でも必要になっている技術だと思うので、いまから入門しておいてもよいかと思います。

おまけ

データサイエンス根性論

Kota UENISHIさん(@kuenishi)が投稿した写真 -