Thread-safety of java.lang.StringBuffer

June 22, 2010 – 6 years, 10 months ago, by Vladimir Klebanov

Short Description:

Show full functional correctness of java.lang.StringBuffer in presence of multithreading.

Code:

From Java standard library

Subbmitted by:

Vladimir Klebanov <vladimir@uni-koblenz.de>


Solution

Tool/method

KeY

Tool version

contact vladimir@uni-koblenz.de

Code/spec

Link

Solution-problem relationship

Only addChar method verified.
Proof theoretically possible for unbounded # of threads, but implementation not correct for N>MAX INT threads (array size limitation in Java)

Tool output

Interactivity, effort needed

few interactions, induction hypothesis easy to find. Effort: 1/2 an hour for experienced user.

How to reproduce

Published

SEFM 2007 (link)

Submitted by

Vladimir Klebanov <vladimir@uni-koblenz.de>