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

[Denys Duchier]

Tom Lord <address@hidden> writes:

> scm_vector_{set,ref} are, indeed, semantically required to be atomic
> operations.   Should the representations provide threads, they must,
> indeed, be implemented with some form of locking.   

There was perhaps a not so obvious point in my remarks about coherence
with an interleaving semantics: while locking is the simplest way to
enforce correctness, it is not always necessary if you know how to
squint in just the right way :-)

First a disclaimer: I have not thought about the issue very long, and
while I have quite a bit of experience with designing concurrent
abstractions, the semantics of concurrency is by no means my area of
expertise.

My suspicion is that it is actually ok to not lock.  A proof is
needed, but it might go along those lines:

Terminology:

        vector                  has a pointer to the vector array
        vector array            contains vector array elements
        vector array element

  - the interesting time points are those where the vector array is
    replaced with a new one

  - an important assumption in my suggestion is that the vector array
    is subject to normal GC and not explicitly recycled when e.g. the
    vector is resized

if V is a vector and it is successively assigned vector arrays A1,
..., An, then these points of assignment are the interesting
timepoints.

The operations on a vector V are:

   vector-ref(V,I)
       1. A = V.array
       2. return A[I]

   vector-set!(V,I,X)
       1. A = V.array
       2. A[I] = X

The issue is what happens for operations when the transition from Ak
to Ak+1 happens between steps 1 and 2? Is there still a way to pretend
that these individual operations are actually executed atomically?

The ordering for the interleaving semantics of concurrent operations
on vector V is determined as follows.  First, each operation is
initiated between some Ak and Ak+1 (i.e. the first step executes when
Ak is the array and before it is replaced by Ak+1).  Let Tk be the
(global) timepoint when V is assigned Ak.  The second step takes place
at (global time) T.  We can order the operations using the
lexicographic order on the pair (Tk,T) for each actual operation: the
point is that the operations _could_ have been executed in this
particular order and would have resulted in the currently observable
state - and (from the language level) we have no way to tell that this
was not what actually took place.  Thus the observable semantics is
consistent with _some_ interleaving.

This is of course very hand-wavy and since it lacks a formal proof, it
could easily be wrong... but you get the idea.

Cheers,

-- 
Dr. Denys Duchier
Équipe Calligramme
LORIA, Nancy, FRANCE