Haha, this is an excellent example! Thanks!
First, just so we agree on the meaning of a frozen function. A frozen function is not the same as a pure function. For example, if you pass in a mutable object to a frozen function, it is permitted to mutate that object. So this is a perfectly fine frozen function:
def counter(sys):
sys.counter += 1
return sys.counter # works if sys isn't immutable
Obviously, this is not the same as your excellent example. The crux in your example is whether it is possible for a frozen function to reach mutable state that was not passed in. The PEP does not permit a frozen function to capture enclosing mutable state (handled by freezing) and throws an exception if a function tries to access globals() directly. Also, in the PEP, immutability is deep, so if sys is immutable above, you can’t traverse it to get to mutable state. But what should we do about imports? The problem is not imports themselves, but the possibility of mutable module state.
Let’s start with what’s in the PEP and then what we envision as part of the future extensions foreshadowed in the PEP.
In the PEP
In the multiple subinterpreters model, each subinterpreter has its own private module state, so if the function is allowed to import the sys module and access module state directly, this is not a race.
In free-threaded Python, this would indeed be a race. In this PEP, I am not so worried about this case. I mean, immutable objects and frozen functions are moving the needle in the right direction — and guaranteeing things in Python is hard!
Looking forward a little
When we add region-based ownership (aka Lungfish – the future, foreshadowed PEP), this race should no longer be possible. The relevant case here is sketched on pages 21 and 22 (slide 16 IIRC) in the presentation we gave at the language summit (https://wrigstad.com/summit-presentation-final.pdf).
With region-based ownership, mutable module state like your counter should be enclosed in one or more regions, and only one thread at a time will be able to access a region’s content. So even free-threaded Python will avoid the data race in your example. If the sys module is not “Lungfish compliant”, it will essentially share a lock with all other non-compliant modules making sure that only one thread at a time accesses state in these modules. This would also avoid the data race.
You can look at sections 5.3.3 and 5.3.4 of this paper that describes the Lungfish design if you are interested in additional details, including freezing of modules that provide only constant immutable state. There’s lots of detail to unpack there for which you may not have the time. But if you do look and you do have questions or find bugs, feel free to – encouraged actually – to reach out.