Python MutableMap should release locks if unhandled exception is raised

[lucasmcdonald3]

Dafny version

4.8.1

Code to produce this issue

Code is here: https://github.com/dafny-lang/dafny/blob/f01af4a4e86a038ed4ea9f81464b2c9bca1955e4/Source/DafnyStandardLibraries/src/Std_Concurrent.py

Command to run and resulting output

lucmcdon@80a997335f93 Desktop % python3
Python 3.11.2 (main, Sep  3 2024, 12:49:51) [Clang 15.0.0 (clang-1500.3.9.4)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> import Std_Concurrent
>>> m = Std_Concurrent.MutableMap()
>>> m.Put(1,2)  # Returns, no output
>>> m.Put(["lists aren't hashable"], "and result in TypeError")
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/lucmcdon/Desktop/testdafny.py", line 45, in Put
    self.map[k] = v
    ~~~~~~~~^^^
TypeError: unhashable type: 'list'
>>> m.Put(1,2)  # Hangs indefinitely

What happened?

The problem is the lock is not released if an exception is raised before the Unlock call.
The solution should be wrapping the internal logic in a try/finally block, ex.

def Put(self, k, v):
    self.lock.Lock__()
    try: 
        self.map[k] = v
    finally:
        self.lock.Unlock()

I tested this locally with the same commands as above, and the final Put no longer hangs.
You should also do this for other methods in the class.

This does not block me or impact me in any way as I don't use this class, but is worth noting.

What type of operating system are you experiencing the problem on?

Mac