Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

There is a thread synchronisation problem in the parser #1155

Open
wadoon opened this issue Dec 23, 2022 · 0 comments
Open

There is a thread synchronisation problem in the parser #1155

wadoon opened this issue Dec 23, 2022 · 0 comments
Labels
KeY Parser 🐞 Bug P:LOW

Comments

@wadoon
Copy link
Member

wadoon commented Dec 23, 2022 •
edited
Loading

This issue was created at git.key-project.org where the discussions are preserved.

  • Mantis: MT-1510
  • Submitted on: 2014-11-21 by (at)mulbrich
  • Updated: 2014-12-20

Description

Under some condition the parser may throw a ConcurrentModificationException
if more than one file is parsed at a time.

Additional Information


This stacktrace is from Jenkin's run 854:
http://abu.se.informatik.tu-darmstadt.de:8080/hudson/job/KeY%20Master/854/testReport/junit/de.uka.ilkd.key.parser/TestParallelParsing/testLoadingOfTwoDifferentProofFiles/


de.uka.ilkd.key.parser.TestParallelParsing.testLoadingOfTwoDifferentProofFiles 

 (file: /home/hudson/jobs/KeY Master/workspace/examples/_testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof; caused by: java.util.ConcurrentModificationException)
	at de.uka.ilkd.key.ui.AbstractUserInterface.load(AbstractUserInterface.java:301)
	at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:262)
	at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:240)
	at de.uka.ilkd.key.parser.TestParallelParsing$LoadThread.run(TestParallelParsing.java:124)
Caused by: java.util.ConcurrentModificationException
	at java.util.ArrayList$Itr.checkForComodification(ArrayList.java:782)
	at java.util.ArrayList$Itr.next(ArrayList.java:754)
	at de.uka.ilkd.key.proof.Node$NodeIterator.next(Node.java:629)
	at de.uka.ilkd.key.proof.Node$NodeIterator.next(Node.java:617)
	at de.uka.ilkd.key.proof.io.DefaultProofFileParser.beginExpr(DefaultProofFileParser.java:136)
	at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15173)
	at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15188)
	at de.uka.ilkd.key.parser.KeYParser.proofBody(KeYParser.java:15096)
	at de.uka.ilkd.key.parser.KeYParser.proof(KeYParser.java:15049)
	at de.uka.ilkd.key.proof.init.KeYUserProblemFile.readProof(KeYUserProblemFile.java:202)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.tryReadProof(ProblemInitializer.java:572)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:439)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:210)
	at de.uka.ilkd.key.ui.AbstractUserInterface.load(AbstractUserInterface.java:287)

Files

allstacktraces.log

a.proof

Notes

(at)mulbrich at 2014-11-21

I ran the test case dozens of times and got an error a ew times.
One like the above, the some 5 times another one:
(I used 6 instead of 2 parallel threads)

Error loading proof.
Line 63, goal 5, rule Use Operation Contract not available or not applicable in this context. (file: /home/m/unison/sync/key/examples/_testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__b()]_JML_normal_behavior_operation_contract_0.proof; caused by: Error loading proof.
Line 63, goal 5, rule Use Operation Contract not available or not applicable in this context. (file: /home/m/unison/sync/key/examples/_testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__b()]_JML_normal_behavior_operation_contract_0.proof; caused by: java.lang.NullPointerException))
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:454)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:210)
at de.uka.ilkd.key.ui.AbstractUserInterface.load(AbstractUserInterface.java:287)
at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:262)
at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:240)
at de.uka.ilkd.key.parser.TestParallelParsing$LoadThread.run(TestParallelParsing.java:128)
Caused by: Error loading proof.
Line 63, goal 5, rule Use Operation Contract not available or not applicable in this context. (file: /home/m/unison/sync/key/examples/_testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__b()]_JML_normal_behavior_operation_contract_0.proof; caused by: java.lang.NullPointerException)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.reportError(DefaultProofFileParser.java:344)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.endExpr(DefaultProofFileParser.java:305)
at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15204)
at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15188)
at de.uka.ilkd.key.parser.KeYParser.proofBody(KeYParser.java:15096)
at de.uka.ilkd.key.parser.KeYParser.proof(KeYParser.java:15049)
at de.uka.ilkd.key.proof.init.KeYUserProblemFile.readProof(KeYUserProblemFile.java:202)
at de.uka.ilkd.key.proof.init.ProblemInitializer.tryReadProof(ProblemInitializer.java:572)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:439)
... 5 more
Caused by: java.lang.NullPointerException
at de.uka.ilkd.key.rule.OneStepSimplifier.simplifyPosOrSub(OneStepSimplifier.java:283)
at de.uka.ilkd.key.rule.OneStepSimplifier.simplifyConstrainedFormula(OneStepSimplifier.java:411)
at de.uka.ilkd.key.rule.OneStepSimplifier.applicableTo(OneStepSimplifier.java:486)
at de.uka.ilkd.key.rule.OneStepSimplifier.isApplicable(OneStepSimplifier.java:531)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.scanSimplificationRule(BuiltInRuleAppIndex.java:131)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.scanModifiedFormulas(BuiltInRuleAppIndex.java:193)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.sequentChanged(BuiltInRuleAppIndex.java:165)
at de.uka.ilkd.key.proof.RuleAppIndex.sequentChanged(RuleAppIndex.java:359)
at de.uka.ilkd.key.proof.Goal.fireSequentChanged(Goal.java:215)
at de.uka.ilkd.key.proof.Goal.setSequent(Goal.java:341)
at de.uka.ilkd.key.proof.Goal.changeFormula(Goal.java:376)
at de.uka.ilkd.key.rule.UseOperationContractRule.apply(UseOperationContractRule.java:880)
at de.uka.ilkd.key.rule.AbstractBuiltInRuleApp.execute(AbstractBuiltInRuleApp.java:78)
at de.uka.ilkd.key.proof.Goal.apply(Goal.java:585)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.endExpr(DefaultProofFileParser.java:293)
... 12 more

I add some more infos on the threads after the failure in an extra file.

I conclude that this exception has to do with static fields in
the one step simplifier and has nothing to do with my recent changes
to the parser.

(at)most at 2014-11-21

I had the same problem on my mostPermissions branch which is based on recent master, see mostPermissions #1 results on Jenkins.

(at)rbubel at 2014-11-21

The static fields in OSS seem not to be critical as they should be all immutable (if I did not miss one).

(at)mulbrich at 2014-11-21

I am sorry. I did not mean the static fields but rather the shared instance
fields. Problem is that OneStepSimplifier is shared between all proofs that
have the same JavaProfile reference.

(at)mulbrich at 2014-11-25

Even if one uses two .proof files that do NOT use the OSS, such an exception
may occur. (I used 2x the attached a.proof)

Line 83, goal 23, rule andLeft not available or not applicable in this context. (file: /home/mattze/unison/sync/key/examples/_testcase/parser/MultipleRecursion/a.proof; caused by: Error loading proof.
Line 83, goal 23, rule andLeft not available or not applicable in this context. (file: /home/mattze/unison/sync/key/examples/_testcase/parser/MultipleRecursion/a.proof; caused by: java.lang.NullPointerException))
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:463)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:219)
at de.uka.ilkd.key.ui.AbstractUserInterface.load(AbstractUserInterface.java:288)
at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:268)
at de.uka.ilkd.key.symbolic_execution.util.KeYEnvironment.load(KeYEnvironment.java:244)
at de.uka.ilkd.key.parser.TestParallelParsing$LoadThread.run(TestParallelParsing.java:124)
Caused by: Error loading proof.
Line 83, goal 23, rule andLeft not available or not applicable in this context. (file: /home/mattze/unison/sync/key/examples/_testcase/parser/MultipleRecursion/a.proof; caused by: java.lang.NullPointerException)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.reportError(DefaultProofFileParser.java:344)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.endExpr(DefaultProofFileParser.java:277)
at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15199)
at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15183)
at de.uka.ilkd.key.parser.KeYParser.pseudosexpr(KeYParser.java:15183)
at de.uka.ilkd.key.parser.KeYParser.proofBody(KeYParser.java:15091)
at de.uka.ilkd.key.parser.KeYParser.proof(KeYParser.java:15044)
at de.uka.ilkd.key.proof.init.KeYUserProblemFile.readProof(KeYUserProblemFile.java:202)
at de.uka.ilkd.key.proof.init.ProblemInitializer.tryReadProof(ProblemInitializer.java:572)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:448)
... 5 more
Caused by: java.lang.NullPointerException
at de.uka.ilkd.key.rule.OneStepSimplifier.simplifyPosOrSub(OneStepSimplifier.java:286)
at de.uka.ilkd.key.rule.OneStepSimplifier.simplifyConstrainedFormula(OneStepSimplifier.java:441)
at de.uka.ilkd.key.rule.OneStepSimplifier.applicableTo(OneStepSimplifier.java:520)
at de.uka.ilkd.key.rule.OneStepSimplifier.isApplicable(OneStepSimplifier.java:565)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.scanSimplificationRule(BuiltInRuleAppIndex.java:131)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.scanAddedFormulas(BuiltInRuleAppIndex.java:175)
at de.uka.ilkd.key.proof.BuiltInRuleAppIndex.sequentChanged(BuiltInRuleAppIndex.java:161)
at de.uka.ilkd.key.proof.RuleAppIndex.sequentChanged(RuleAppIndex.java:359)
at de.uka.ilkd.key.proof.Goal.fireSequentChanged(Goal.java:215)
at de.uka.ilkd.key.proof.Goal.setSequent(Goal.java:341)
at de.uka.ilkd.key.rule.FindTaclet.apply(FindTaclet.java:273)
at de.uka.ilkd.key.rule.TacletApp.execute(TacletApp.java:445)
at de.uka.ilkd.key.proof.Goal.apply(Goal.java:585)
at de.uka.ilkd.key.proof.io.DefaultProofFileParser.endExpr(DefaultProofFileParser.java:272)
... 13 more

(at)mulbrich at 2014-12-20

I added some instrumentation to the code and found out that in all cases in
which I observed an exception, one of the parallel load operation has already
finished parsing and replaying.

I guess that the clean-up code after replaying resets some static value which
makes parallel applications crash.

History

  • (at)mulbrich -- (NEW_BUG) 2014-11-21

  • (at)mulbrich -- (BUGNOTE_ADDED) 2014-11-21

  • (at)mulbrich -- (FILE_ADDED) 2014-11-21

  • (at)most -- (BUGNOTE_ADDED) 2014-11-21

  • (at)rbubel -- (BUGNOTE_ADDED) 2014-11-21

  • (at)mulbrich -- (BUGNOTE_ADDED) 2014-11-21

  • (at)mulbrich -- (BUGNOTE_ADDED) 2014-11-25

  • (at)mulbrich -- (FILE_ADDED) 2014-11-25

  • (at)grahl -- (NORMAL_TYPE) 2014-12-16

  • (at)mulbrich -- (BUG_MONITOR) 2014-12-20

  • (at)mulbrich -- (BUGNOTE_ADDED) 2014-12-20

Attributes

  • Category: Parser
  • Status: CONFIRMED
  • Severity: MINOR
  • OS:
  • Target Version:
  • Resolution: OPEN
  • Priority: LOW
  • Reproducibility: RANDOM
  • Platform:
  • Commit: b6939e9325ae63923defe6bc7036e8f5e517280e
  • Build:
  • Tags []
  • Labels: ~KeY Parser ~Bug ~LOW

View in Mantis

Information:

  • created_at: 2017-05-29T02:57:42.734Z
  • updated_at: 2021-02-10T14:42:50.397Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 1
@wadoon wadoon changed the title <placeholder> There is a thread synchronisation problem in the parser Dec 24, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
KeY Parser 🐞 Bug P:LOW
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@wadoon