[pypy-dev] pre-emptive micro-threads utilizing shared memory message passing?

[William Leslie]

On 28 July 2010 23:37, Paolo Giarrusso <p.giarrusso at gmail.com> wrote:
> On Wed, Jul 28, 2010 at 14:54, William Leslie
> <william.leslie.ttg at 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