On 28 July 2010 23:37, Paolo Giarrusso <p.giarrusso@gmail.com> wrote:
On Wed, Jul 28, 2010 at 14:54, William Leslie <william.leslie.ttg@gmail.com> wrote:
Does anyone know if there is a central resource for incompatible python memory model proposals? I know of Jython, Python-Safethread, and Mont-E.
Add Unladen Swallow to your list - the "Jython memory model" is undocumented. I don't know of Mont-E, can't find its website through Google (!), and there seems to be no such central resource.
Mont-E was, for a long time, the hypothetical capability-secure subset of python based on E and discussed on cap-talk. A handful of people started work on it in earnest as a cpython fork fairly recently, but it does seem to be pretty quiet, and documentation free. I did find a repository and a presentation: http://bytebucket.org/habnabit/mont-e/overview https://docs.google.com/present/view?id=d9wrrrq_15ch78nq9n
This is a general issue with concurrency, and usually I try to solve this using more pencil-and-paper design than usual.
I found the following paper pretty interesting. The motivating study is some concurrency experts implementing software for proving the lack of deadlock in Java. Even with the sort of dedication that only a researcher with no life can provide, their deadlock inference software itself deadlocked after many years of use. www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-1.pdf
An example for MiniAxon (as I understand it, which is not very well) would be verification that a "task" (including functions that the task calls) never closes over and yields the same mutable objects, and never mutates globally reachable objects.
I guess that 'close over' here means 'getting as input'.
I mean that it keeps a reference to the objects between invocations. Hence, sharing mutable state.
The trouble is that it is so hard to work out what immutable really means. Non-optional annotations would be not very pythonian.
If you want static guarantees, you need a statically typed language. The usual argument for dynamic languages is that instead of static typing, you need to write unit tests, and since you must do that anyway, dynamic languages are a win.
One thing that many even very experienced hackers miss is that (static) types (and typesystems) actually cover a broad range of usages, and many of them are very different to the structural typesafety systems you are used to in C# and Java. A typesystem can prove anything that is statically computable, from the noninterference of effects to program termination, the ability to stack allocate data structures, and that privileged information can't be tainted. It's important to realise that these are orthogonal to, not supersets of, typesystems that validate structural safety. So it can be reasonable, if yet a little more difficult, to apply them to dynamic languages. -- William Leslie