Repository navigation
Fix RAC IllegalAccessError in Atomic{Long,Integer,Boolean} constructor specs - #29
Closed
bernardladenthin wants to merge 1 commit into
Closed
bernardladenthin wants to merge 1 commit into
bernardladenthin wants to merge 1 commit into
Conversation
bernardladenthin
force-pushed
the
fix/rac-atomiclong-private-value-access
branch
from
September 30, 2026 20:55
ade0017 to
4ebda9c
Compare
bernardladenthin
changed the title
8 of 9 tasks
davidcok
added a commit
that referenced
this pull request
Oct 5, 2026
…AndSet omitted - RAC: the constructors, set and lazySet state their postconditions on the private field value only for ESC (-RAC), and through get() for RAC (+RAC), extending #29; get() is a helper. - AtomicLong.getAndAdd: ensures value == \old(value) + v (was value == v, which let ESC prove false results). - AtomicLong.accumulateAndGet: \result is the new value (was \old(value)). - AtomicLong.getAndUpdate: ensures \result == \old(value) (was 'true'). - AtomicInteger/AtomicLong.lazySet: the same postcondition as set (was 'true'). - weakCompareAndSet is omitted from all three: it is deprecated (since Java 9), and its spec claimed it always succeeds when the value matches, which Java does not guarantee. Tested by OpenJMLTest/testspecs java-util-concurrent-atomic-* (SpecsEsc and SpecsRac). Co-Authored-By: Claude Opus 5.5 <[email protected]>
Member
|
Merged via dev-21: this commit (4ebda9c) is on Specs dev-21, where c365293 extends it (RAC-safe Atomic{Boolean,Integer,Long} specs, spec fixes, weakCompareAndSet omitted). OpenJML's testspecs cases from OpenJML/OpenJML#982 pass with it (SpecsEsc, SpecsRac, SpecsBase). It will reach master-21 with the next merge of dev-21. |
5 of 7 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The
Atomic{Long,Integer,Boolean}constructor specs reference the privatejava.basefield
valuein unguarded clauses (ensures value == v/== 0). RAC checks them at thecall site;
spec_publicis only honoured for classes RAC compiles itself(
JmlAssertionAdderflips the flag to public), so the client emitsgetfield AtomicLong.valueand throwsIllegalAccessErroron anynew AtomicLong()(also on OpenJML's own JVM;
--add-opensdoes not help, it only affects reflection).Fix, following the existing idioms of these files:
AtomicLong,AtomicInteger:ensures get() == v(asset()/intValue()already do).ESC-equivalent, since
get()has-RAC ensures \result == value.AtomicBoolean:-RAC ensures value == (v ? 1:0)++RAC ensures get() == v(as
get()does). A plainget() == vwould losevalue ∈ {0,1}:new AtomicBoolean(true).compareAndSet(true, false)is then no longer provable.Verified with 21.0.27 (Windows): RAC red before / green after for all three classes;
ESC output unchanged. Tests: OpenJML/OpenJML#982 (testspecs, SpecsEsc + SpecsRac).
Base:
master-21(the branch OpenJML 21.x builds against).Found via OpenJML RAC on https://github.com/bernardladenthin/streambuffer