GNU Time にある壮大なバグ (はもうありませんので安心してください) #Linux

とりあえず警告として拡散できればということで。

bash の time ではなく、明示的に /usr/bin/time と書くことで呼び出せる
プログラムがあります。機能はtime と同じく、コマンドを引数に取り、
それを実行し、そして使用メモリ量、使用時間(user,sys)を出力します。

bashのtimeにくらべて、引数でフォーマットを自由に変更できるので便利です。
しかししかし、壮大なバグがあります。

それはすなわち、

使用メモリ量が4倍に表示される

ことです。BSDの実装をlinuxにそのまま持ってきたらこうなったそうです。
2010年ぐらいに見つかったバグですが、
ubuntu14.04の公式aptリポジトリでも time のバージョンは1.7のまま。
直っていません。直せよ・・・。

論文締め切り前なんですが、これで結構な時間を無駄にしました。ちくしょー