tc39 / proposal-ecmascript-sharedmem

Shared memory and atomics for ECMAscript
Mozilla Public License 2.0
375 stars 32 forks source link

Definition of "lock-free" #131

Closed jfbastien closed 7 years ago

jfbastien commented 8 years ago

The definition of "lock-free" doesn't seem very solid:

Formally, atomic operations are lock-free if, infinitely often, some atomic operation finishes in a finite number of program steps. In practice, if an atomic operation is implemented with any type of lock the operation is not lock-free. Lock-free does not imply wait-free: there is no upper bound on how many machine steps may be required to complete a lock-free atomic operation.

That an atomic access of size n is lock-free does not imply anything about the (perceived) atomicity of non-atomic accesses of size n, specifically, non-atomic accesses may still be performed as a sequence of several separate memory accesses. See ReadSharedMemory and WriteSharedMemory for details.

A few comments:

C++ defines "lock-free" as:

\pnum
Executions of atomic functions
that are either defined to be lock-free~(\ref{atomics.flag})
or indicated as lock-free~(\ref{atomics.lockfree})
are \defnx{lock-free executions}{lock-free execution}.

\begin{itemize}
\item
  If there is only one thread that is not blocked~(\ref{defns.block})
  in a standard library function,
  a lock-free execution in that thread shall complete.
  \begin{note}
    Concurrently executing threads
    may prevent progress of a lock-free execution.
    For example,
    this situation can occur
    with load-locked store-conditional implementations.
    This property is sometimes termed obstruction-free.
  \end{note}
\item
  When one or more lock-free executions run concurrently,
  at least one should complete.
  \begin{note}
    It is difficult for some implementations
    to provide absolute guarantees to this effect,
    since repeated and particularly inopportune interference
    from other threads
    may prevent forward progress,
    e.g.,
    by repeatedly stealing a cache line
    for unrelated purposes
    between load-locked and store-conditional instructions.
    Implementations should ensure
    that such effects cannot indefinitely delay progress
    under expected operating conditions,
    and that such anomalies
    can therefore safely be ignored by programmers.
    Outside this International Standard,
    this property is sometimes termed lock-free.
  \end{note}
\end{itemize}
lars-t-hansen commented 8 years ago

Fair point. The "infinitely often" formalization is from Herlihy & Shavit, "The art of multiprocessor programming". I'm not jazzed about it myself, it's hard to figure out exactly what it means, hence the "in practice" comment, which is probably too loose to have teeth.

lars-t-hansen commented 7 years ago

I see the current prose is just the same as the old prose, https://tc39.github.io/ecma262/#sec-agents. @syg, your opinion about this?

syg commented 7 years ago

@lars-t-hansen Since it's in an informative note, I'm not worried about its having teeth or not. As it stands now, that "formally" comment reads like a throwaway sentence, and the whole section about lock-free-ness really doesn't say anything more than the obvious implementation interpretation, i.e., "implemented with a mutex that can block".

I am currently leaning towards deleting the "formally" sentence and leaving the "does not imply wait freedom" part. Thoughts?

lars-t-hansen commented 7 years ago

@syg, created a PR, LMK what you think.

lars-t-hansen commented 7 years ago

The PR was merged.