fixedpoint.jp




2015/02/26

Timsort 実装のバグが形式的手法で見つかったけれど...

Java や Python で広く利用されている Timsort というソートアルゴリズムの実装のバグを形式的手法で見つけたというニュースがありました: http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/

Design by Contract の考え方に基づいた KeY というツールで正しさを検証しようとしたところ、証明できなかったのでよく調べてみたらバグがあったということです。KeY では関数が評価される際の事前条件と事後条件、および不変条件を表現でき、関数内の全てのパスでこれらの条件が成り立っているかどうかを静的に証明できるそうです。

冒頭の記事に書かれているように、発見者は OpenJDK プロジェクトに詳細と修正案を報告したのですが、その反応は期待通りではなかったようです:

The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space. Given the astronomical number of program runs that such a central routine is used in, this leads to a considerable waste of energy. As to the reasons, why our solution has not been adopted, we can only speculate: perhaps the JDK maintainers did not bother to read our report in detail, and therefore don’t trust and understand our fix. After all, Open Java is a community effort, largely driven by volunteers with limited time.

実際のバグ報告を見てみると、実は発見者自身が2つの修正案を示しており、コミットされた修正はその1つ(現実的なケースにおいて十分なメモリを確保するように変更)を採用しています。そのため、発見者が採用して欲しかったもう1つの案が無視された形になったということです。

しかし、これはバグ報告のためのコミュニケーションに改善の余地があったと言えそうです。おそらく報告の中で単独の修正案を示していたら、それが採用された可能性が高かったはずです。(さらにパッチとして提供されていたらさらに望ましかったはずです。というのも、その変更による影響範囲がどれくらいかを確認するのに差分の形が便利だからです。)また、発見者が想像から言及している "volunteers with limited time" というのもやや乱暴です。なぜなら、今回修正を担当した開発者も(メールアドレスから判断すると)Oracle に所属しており、職務の一環として活動していると考えられるためです。

今回の教訓としては、例え形式的手法で不具合を発見し証明できても、望ましい修正を提案する過程が重要であることは変わらない、ということになります。

#permalink

2015/02/24

SRFI 121と eof object

SRFI 121: Generators は、一般に羃等でない手続きを generator として扱うための API を定義しています。このような手続きは、繰り返し呼ばれる度ごとに値を生成していると考えることができます。あるいは、ある特定の集合から順番に値を返すものと見なすことができ、有限集合の場合は全ての値を返したら終了することになります。

この SRFI では、終了の印に eof object を用います。つまり、その手続きから eof object が返ってきたら終了となります。ファイル port から入力する際に末尾に到達したことを知らせる仕組みと似せています。

Scheme では、eof object は独自の型を持つ特別なオブジェクトです。このようなオブジェクトは、空リストと eof object だけです。

R5RS では eof-object? という述語だけがありました。R6RS で disjoint type となり、個別のオブジェクトを作成できるようになりました。R7RS-small も R6RS を踏襲しています(ただし R6RS と異なり、eof object 間の同値性については規定されていません)。

このような SRFI で利用されるなど、eof object の発展がうかがえます。

#permalink

2015/02/17

SRFI-118 と可変長文字列

SRFI 118: Simple adjustable-size strings は新たな手続きとして string-append!string-replace! という2つを提案しています。これだけ見ると特に驚きはないようですが、実際は Specification 節冒頭で

The standard Scheme functions make-string and string-copy are specified to return variable-size mutable strings by default.

というところで標準の手続きに対して大きな要求をしています。

R5RS では string は原則(string-set!string-fill!による制限付きの操作を除き)immutable であり、当然 string オブジェクトが作成された時点で長さは固定されていました。R6RS でもそれは同じで、mutable strings ライブラリ((rnrs mutable-strings (6)))でも固定長であることは維持されていました。R7RS-small も R5RS を踏襲しています。

つまりこの SRFI は string を mutable どころか可変長にできるようにしようという大胆なものといえます。

#permalink

2015/02/13

SRFI-120: Timer APIs について

今や HTML5でさえ timer の API があるのに、Scheme にないわけにはいかない、という SRFI-120

参考

#permalink

Archives

2014: Dec / Nov / Oct / Aug / Apr / Mar / Feb / Jan

2013: Dec / Nov / Oct / Sep / Aug / Jun / May / Apr / Mar

2012: Nov / Oct / Sep / Jul / Jun / May / Mar / Feb / Jan

2011: Dec / Nov / Oct / Sep / Jul / Jun / Apr / Mar / Feb / Jan

2010: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2009: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2008: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2007: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2006: Dec / Nov / Oct / Sep


© 2006-2015 fixedpoint.jp