Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ConcurrentModificationException in UI Code [wa...

view this post on Zulip Email Gateway (Apr 25 2024 at 09:14):

From: Salomon Sickert-Zehnter <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle Community,

I’m currently testing Isabelle2024-RC2 on macOS Sonoma (14.4.1, Apple M1 Max) and I wanted to report a newly appearing Java exception. Compared to Isabelle2023 I now regularly get reports of an ConcurrentModificationException processing the token markup (all stack traces so far have been identical). jEdit does not crash and continues to run, but it seems that there is unsynchronised access to a HashMap. The full stack trace is at the bottom. I hope this helps identifying the cause of this unsynchronised access.

Best regards,
Salomon

17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: Error repainting line range {0,26}:
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: java.util.ConcurrentModificationException
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.base/java.util.HashMap.computeIfAbsent(HashMap.java:1229)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.syntax.Chunk.init(Chunk.java:539)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.syntax.DisplayTokenHandler.initChunk(DisplayTokenHandler.java:175)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.syntax.DisplayTokenHandler.initChunks(DisplayTokenHandler.java:184)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.syntax.DisplayTokenHandler.makeScreenLine(DisplayTokenHandler.java:392)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.syntax.DisplayTokenHandler.handleToken(DisplayTokenHandler.java:96)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at isabelle.jedit.Token_Markup$Marker.markTokens(token_markup.scala:296)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.buffer.JEditBuffer.markTokens(JEditBuffer.java:2724)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.buffer.JEditBuffer.markTokens(JEditBuffer.java:1387)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.textarea.ChunkCache.lineToChunkList(ChunkCache.java:828)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.textarea.ChunkCache.updateChunksUpTo(ChunkCache.java:702)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.textarea.ChunkCache.getLineInfo(ChunkCache.java:266)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.textarea.ExtensionManager.paintScreenLineRange(ExtensionManager.java:105)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.textarea.Gutter.paintComponent(Gutter.java:193)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1128)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.scala$swing$Component$SuperMixin$$super$paintChildren(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paintChildren(Component.scala:72)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paintChildren$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.__super__paintChildren(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component.paintChildren(Component.scala:261)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paintChildren(Component.scala:69)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paintChildren$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.paintChildren(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.scala$swing$Component$SuperMixin$$super$paint(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paint(Component.scala:78)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paint$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.__super__paint(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component.paint(Component.scala:267)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paint(Component.scala:75)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paint$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.BorderPanel$$anon$1.paint(BorderPanel.scala:51)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.scala$swing$Component$SuperMixin$$super$paintChildren(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paintChildren(Component.scala:72)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paintChildren$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.__super__paintChildren(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component.paintChildren(Component.scala:261)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paintChildren(Component.scala:69)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paintChildren$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.paintChildren(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.scala$swing$Component$SuperMixin$$super$paint(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paint(Component.scala:78)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.__super__paint$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.__super__paint(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component.paint(Component.scala:267)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paint(Component.scala:75)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.Component$SuperMixin.paint$(Component.scala:55)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at scala.swing.TabbedPane$$anon$1.paint(TabbedPane.scala:79)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at org.gjt.sp.jedit.gui.DockableWindowManagerImpl.paintChildren(DockableWindowManagerImpl.java:638)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintChildren(JComponent.java:961)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paint(JComponent.java:1137)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintToOffscreen(JComponent.java:5318)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.RepaintManager$PaintManager.paintDoubleBufferedImpl(RepaintManager.java:1656)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.RepaintManager$PaintManager.paintDoubleBuffered(RepaintManager.java:1631)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.RepaintManager$PaintManager.paint(RepaintManager.java:1569)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.RepaintManager.paint(RepaintManager.java:1336)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent._paintImmediately(JComponent.java:5266)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.JComponent.paintImmediately(JComponent.java:5076)
17:29:02 [AWT-EventQueue-0] [error] ExtensionManager: at java.desktop/javax.swing.RepaintManager$4.run(RepaintManager.java:878)
17:29:02 [AWT-EventQueue-0] [error] Extension
[message truncated]

view this post on Zulip Email Gateway (Apr 25 2024 at 11:52):

From: Makarius <makarius@sketis.net>
Thank you for testing Isabelle release candidates. Based on the Java
exeception trace, I have made a patch for "isabelle component_jedit" (which is
attached for the record).

The resulting jedit.jar is available here:
https://files.sketis.net/jedit-20240425/jedit.jar --- if you copy that over
Isabelle2024-RC2.app/contrib/jedit-20231120/jedit5.6.0-patched/jedit.jar you
can try that out.

I have only made a few sanity tests so far. It might behave differently on
very large and ambitious theory files. I might be also better to avoid
synchronization and silently ignore concurrent updates of the cache.

Makarius

ch

view this post on Zulip Email Gateway (Apr 26 2024 at 14:59):

From: Salomon Sickert-Zehnter <cl-isabelle-users@lists.cam.ac.uk>
Thank you for quickly addressing this. So far I did not observe any regressions and I’ll let you know in case I encounter one.

Best regards,
Salomon Sickert-Zehnter

—
Salomon Sickert-Zehnter (s_sickertzehnter@apple.com)
 SEG FV Security

Last updated: May 04 2024 at 20:16 UTC