Where do I find the GUI Effect base case?

[Jo D]

I'm trying to find out what the actual GUI Effect annotations on the JDK are.

I need them for two things:

1. To better understand what objects are protected by @UIEffect.
   (E.g. are property handler updates under @UIEffect? What is the policy for the UI classes that do the L&F? We need to validate assumptions, and if there's unexpected behaviour we need to know the intentions so we can report any stub file bugs.)
2. To be able to distinguish whether an unexpected GUIEffect error is a falsified assumption on our side, or a bug in the checker.
3. To be able to annotate our own Swing classes in a way that's consistent with the induction base (otherwise we'll just get tons of false positives).
   We have subclasses of Swing (AWT, actually) Component,
   we have message handlers,
   we have Graphics2d objects (in our Look&Feel classes, mostly);
   it turned out that we don't always have a clear view of what's @GUIEffect and what's @SafeEffect.

I'll accept the specification of the base case in any form, even if I have to read source code and ask more questions ;-)

Regards,

Jo

[Colin Stebbins Gordon]

Currently there seems to be a bug with the jdk stubs. After your last email about this I looked and saw that currently there is no JDK11 stub file.  Some things were migrated out of the JDK8 stubfile but got lost in the shuffle somewhere.  A corrected version should look closer to https://github.com/typetools/checker-framework/blob/bb3be09e0116cfdf6c47dbc0cf08536328d6fb03/checker/src/main/java/org/checkerframework/checker/guieffect/jdk.astub but I would need to do some digging to make sure restoring that is sensible (verifying they're still valid).

The underlying philosophy behind the original annotations was:

• The overwhelming majority of methods in AWT should be @UIEffect since they'll throw an exception when called from another thread.  Consequently, most subpackages of java.awt are marked @UIPackage, with selective overriding for methods that are actually safe (e.g., invokeLater).
• Err on the side of soundness by refining annotations to mark more things safe over time if they're found to cause problems.

Property handler updates are one of the generally tricky idioms found during the original design process for the system.  The main sticking point back then was actually some property updates in Eclipse's UI library, which were tricky because Eclipse has a global property store whose updates fire on whatever thread updates the modified property (or at least, had this design at the time). Then since the same global object was updated from lots of threads, this caused a lot of false positives.  There's an example in the commit linked above (PropertyChangeSupport) of how if the property stores are split into ones used by the UI thread and ones for background threads, then @PolyUIType is enough to make things work out okay.

In general, the current stubs cover a relatively small slice of AWT and Swing, so if (once I check about restoring some of the old stub contents) you discover annotations you disagree with, or missing annotations, I'd be happy to hear about them.

-Colin

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/a17087b6-91c9-462a-8fef-1d30fece3388n%40googlegroups.com.

[Jo D]

Hmm... yes, you'd have to tell the checker not to look at the property store as a whole; it would have to treat each property as a separate variable.

If that's the route, the GUI Effect checker should have annotations that allow specifying which properties are @SafeEffect and which are @GUIEffect, too.

Correction: Obviously the property store as a whole is still a variable that's either @SafeEffect or @UIEffect.

And if the property store as a whole is @UIEffect, there should be locking mechanisms that allow individual properties to be @SafeEffect anyway. 

[Jo D]

About reporting annotation corrections: That's hard to do for me.

The thing is that the descriptions in the manual about what the annotations mean are a bit unclear to me, so I have been thinking that I should probably take the existing annotations as a reference to figure out these details.

Now if neither the manual nor the annotations are a specification that one can work with unassisted, that's a bit of shifting ground.

Not sure what the best way forward would be. I can imagine doing two things:

• Work with you to clarify the manual.
  I know a bit about how software engineering and formal logic connect, so I can contribute a pretty confident vote about what aspects are covered how well.
  That's a compact but intense effort, and would have to be done in the next few days (or I might find more time three months later, we have a rule that we get an innovation sprint of two weeks every three months).
• Do an ad-hoc question whenever I'm unsure.
  It's going to impede our work of adopting GUI Effect checker to our application significantly (which may or may not be relevant to you).

Regards,

Jo

[Colin Stebbins Gordon]

Certainly the intent is not for the annotations to change frequently; they're targeting pretty stable APIs after all.

I'm happy to work to improve the documentation; if you have questions then I'm sure others either have the same questions or would in the future, and ultimately such improvements would help avoid future confusion for everyone. Based on your other email from today (I'll have to respond to that one tomorrow) I can definitely see things to clarify, as well as some possible feature additions that would mesh well with what's currently implemented.

What exactly is your timeline? A midway point would be for you and me to have an intensive Q&A session to work out needed clarifications and give answers; polished prose would take longer.

To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/66dc1734-ca4b-4726-82c9-09aa567a8225n%40googlegroups.com.

[Durchholz, Joachim]

Timeline:

I can’t do much today and on Monday, I’ll be available for the rest of the week, afternoons CEST.

The next opportunity for me to do anything meaningful would be two weeks in September, that’s the next slot where I have a time budget for “innovation”.

I could spend a few hours of private time on this during the upcoming weekend if necessary.

 

Re documentation improvement:

I have some pretty solid background at technical documentation, and I already have some ideas what could be done with the documentation even if no annotation renaming shenanigans are going to happen.

(Two, actually: (1) Restructure the CF manual sections so that the first section is just a high-level teaser that tells the reader what it does and gives keywords, then a section about @UIEffect/@SafeEffect, then a section about the polymorphic stuff. (2) Document for each annotation what effect it has if a developer places it in the code, plus how it interacts with other annotations.)

 

Regards,

Jo

To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/CAF5TXPc09MPqNkjv8FKU10fOpuX9sKVj-Hk0wdUKLqpORABGeQ%40mail.gmail.com.

 

Sensitivity: C2 Internal

The content of this e-mail is intended only for the confidential use of the person addressed.
If you are not the intended recipient, please notify the sender and delete this e-mail immediately.
Thank you.

[Jo D]

Now that I know where the annotated sources are, I could download them and extract an overview so I can look up the CF annotations.

I use it for quickly checking what annotations have been placed; I'm posting it here as a data point for the CF team when it considers reporting facilities:

----------------------------------------------------------------------

@UIPackage package java.awt

public abstract @UsesObjectEquals @UIType Component

    @SafeEffect public void repaint()

    @SafeEffect public void repaint(int x, int y, int width, int height)

    @SafeEffect public void repaint(long tm)

    @SafeEffect public void repaint(long tm, int x, int y, int width, int height)

public @UIType class Container

    @SafeEffect @Override public void invalidate()

public @UsesObjectEquals class Desktop

    @SafeEffect public void browse(URI uri)

    @SafeEffect public void edit(File file)

    @SafeEffect public static synchronized Desktop getDesktop()

    @SafeEffect public static boolean isDesktopSupported()

    @SafeEffect public boolean isSupported(Action action)

    @SafeEffect public void mail()

    @SafeEffect public void mail(URI mailtoURI)

    @SafeEffect public void open(File file)

    @SafeEffect public void print(File file)

@UIType @AnnotatedFor({"interning"}) public @UsesObjectEquals class java.awt.EventQueue

    @SafeEffect public static void invokeLater(@UI Runnable runnable) {

----------------------------------------------------------------------

@UIPackage package java.awt.dnd

----------------------------------------------------------------------

@UIPackage package java.awt.event

@AnnotatedFor({"guieffect"}) @UIType public interface java.awt.event.ActionListener

----------------------------------------------------------------------

package java.beans

@AnnotatedFor({"fenum", "guieffect","interning", "nullness"}) @PolyUIType public @UsesObjectEquals class PropertyChangeSupport

    @PolyUIEffect public void addPropertyChangeListener(@PolyUI PropertyChangeSupport this, @Nullable @PolyUI PropertyChangeListener listener)

    @PolyUIEffect public void addPropertyChangeListener(@PolyUI PropertyChangeSupport this, @Nullable String propertyName, @Nullable @PolyUI PropertyChangeListener listener)

    @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, int index, boolean oldValue, boolean newValue)

    @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, int index, int oldValue, int newValue)

    @PolyUIEffect public void fireIndexedPropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, int index, @Nullable Object oldValue, @Nullable Object newValue)

    @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, PropertyChangeEvent event)

    @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, boolean oldValue, boolean newValue)

    @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, @FenumTop int oldValue, @FenumTop int newValue)

    @PolyUIEffect public void firePropertyChange(@PolyUI PropertyChangeSupport this, String propertyName, @Nullable @FenumTop Object oldValue, @Nullable @FenumTop Object newValue)

    @PolyUIEffect public @PolyUI PropertyChangeListener[] getPropertyChangeListeners(@PolyUI PropertyChangeSupport this)

    @PolyUIEffect public @PolyUI PropertyChangeListener[] getPropertyChangeListeners(@PolyUI PropertyChangeSupport this, String propertyName)

    @PolyUIEffect public boolean hasListeners(@PolyUI PropertyChangeSupport this, @Nullable String propertyName)

    @SafeEffect public PropertyChangeSupport(@PolyUI @UnknownInitialization(Object.class) Object sourceBean)

    @PolyUIEffect public void removePropertyChangeListener(@PolyUI PropertyChangeSupport this, @Nullable PropertyChangeListener listener)

    @PolyUIEffect public void removePropertyChangeListener(@PolyUI PropertyChangeSupport this, @Nullable String propertyName, @Nullable PropertyChangeListener listener)

----------------------------------------------------------------------

package java.lang

@AnnotatedFor({"aliasing", "guieffect", "index", "lock", "nullness"}) @PolyUIType public class Object

    @GetClass @SafeEffect @Pure @HotSpotIntrinsicCandidate public final native Class<?> getClass(@PolyUI @GuardSatisfied @UnknownInitialization Object this);

@AnnotatedFor({"guieffect", "nullness"}) @PolyUIType @FunctionalInterface public interface Runnable

    @PolyUIEffect public abstract void run(@PolyUI Runnable this);

----------------------------------------------------------------------

@UIPackage package javax.swing

@AnnotatedFor({"interning", "guieffect", "nullness"}) @UIType @JavaBean(defaultProperty = "UIClassID") @SuppressWarnings("serial") public abstract class JComponent

    @SafeEffect public void revalidate()

@AnnotatedFor({"guieffect"}) @UIType public class SwingUtilities

    @SafeEffect public static void invokeAndWait(final @UI Runnable doRun)

    @SafeEffect @SuppressWarnings("deprecation") public static void setLookAndFeel(String className)

----------------------------------------------------------------------

@UIPackage package javax.swing.event

----------------------------------------------------------------------

@UIPackage package javax.swing.text