pika-dev
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Pika-dev] Guile FFI: resizable vector problem


From: Tom Lord
Subject: Re: [Pika-dev] Guile FFI: resizable vector problem
Date: Tue, 3 Feb 2004 16:47:37 -0800 (PST)



    > From: Denys Duchier <address@hidden>

    [argument that locking can be avoided for vectors because,
     absent locking, the observable results are consistent
     with some order of execution.]


Let me restate your argument just to make sure I've received you
correctly.  I'll be using pretty informal notation.

You're modeling a vector as having a function:

        array(vector) -> array_address

So an operation like vector_set is:

        1: ar = array(vector);
        2: ar[x] = value;

And vector_resize is something like:

        1: array(vector) = realloc (array(vector),newsize)

and you're reasoning about what happens if vector_set and
vector_resize are executed concurrently.

A few observations:

First, the granularity of atomicity is an issue.   For example,
consider what happens if vector_set:1 ("vector_set, step 1") is
executed concurrently with vector_resize:1.

Many actual machines will guarantee a serial ordering of the two steps
-- but C does not.  Portable C must employ locking for that reason --
though a non-(formally)-portable representations-layer implementation
wouldn't have to.  That's not obviously much of an objection -- a big
optimization that applied only, to say, x86-family architectures is
still valuable.

Second: from the point of view of _Scheme_ semantics -- all concurrent
executions of vector_set and vector_resize have the same result: the
assignment takes place and is apparent in the final result.  Locking
is necessary for that reason, too.  This objection is, I think,
unsurmountable.

    > This is of course very hand-wavy 

No sweat.

    > and since it lacks a formal proof, it
    > could easily be wrong... 

Sadly, yes.

    > but you get the idea.

Right.  It's the right kind of thing to look for.  Just not a correct
example.

-t






reply via email to

[Prev in Thread] Current Thread [Next in Thread]