Copyright © (2002) by Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distrubuted for profit or commericial advantage. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee.
We are concerned with the problem of verifyng ("certifying") whether the client of a software component conforms to the component's constraints for correct usage. We focus here on the Concurrent Modification Problem (CMP), a component-client conformance problem that can occur when certain classes defined by the Java Collections Framework are misused. Since CMP errors arise from relationships among a potentially unbounded number of objects, the problem cannot be define as a simple finite-state property. Instead, we show that it is natural to specify it as a particular must-alias property for an abstract heap manipulated by the component. Computing this must-alias property would seem to be difficult, since the problem is contained in a class known to be intractable. However, we show that by exploiting the fact that the component's abstract heap is manupulated only through a well-defined interface, we can systematically derive efficient and accurate cerfification algorithms for CMP. For a restricted, but still quite useful class of client programs, we can perform precise interprocedural certificaiton in polynomial time. We then generalize the approach to arbitrary client programs. Although this generalization yields some loss of precision in principle, the results produced by our ptototype implementation of the certification algorithm in practice are quite accurate for the suite of benchmark programs studied. We believe the techniques presented here are likely to be applicable to other conformance problems as well.
By: G. Ramalingam, Alex Warshavsky, John H.. Field, Mooly Sagiv
Published in: ACM SIGPLAN Notices, volume 37, (no 5), pages 83-94 in 2002
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .