Software Transactional Memory

最近看了一下这篇文章，应该是STM的开山之作。下面是看的时候随手记下来的东西，可能有很多错误的单词。另外，文章中的代码很难看懂，分在几页上，为了方便阅读，也抄了下来。
Software transactional memory
    1. STM is non-blocking, implemented on existing machines using
    Load_linked/Store_conditional. STM provides an highly concurrent method to
    translate sequential objects into non-blocking ones based on a k-word
    compare and swap.
    2. In multiprocessor systems, unpredictable delay is an increasingly serious
    problem. Conventional techniques for implementing concurrent objects by
    means of critical sections are unsuitable. To get highly concurrent, we need
    non-blocking methods. Howere, existing non-blocking methods are not
    practicle in current machines.
    3. Herlihy and Moss proposed "Transactional Memory" in hardware. However,
    their method is blocking.
    4. Author proposed STM aimed at static transactions --transactions which
    access a pre-determined sequence of locations.
    5. In a transactional apoach, the key to keep live in a faulty enviroment
    is "helping" method. In order to free a location, one need only help its
    single owner transaction to complete. To avoid the overhead of coordination
    among several transactions attempting to help releasing a location, employ
    "reactive" policy "non-redundant-helping"       
    6. Translating a sequential share object implementation into a non-blocking
    one is straightforward: use transactional memory to implement any collection
    of changes to a shared object, performing them as an atomic k-work
    Compare&Swap transaction on the desired locations.
    7. Herlihy's method: to update a data structure, first copy it to a new
    block of memory, make the changes to the copy, tentatively switching the
    pointer to the new copy, with help of load_linked/store_conditional
    operations.
    8. Barnes' caching method: very similar to k-word Compare&Swap, but using a
    cooperative method to achieve liveness. This method has a recursive
    structure of "help", this cause the performance penalty.
    9. A transaction is a finit sequence of local and shared memory machine
    instructions:
        Read-transactional: reads a value of a shared location into a local
        register;
        Write-transactional: store the content of a local register into a shared
        memory location.
    10. The data set of a transaction is the shared locations accessed by above
    instructions in this transaction.
    11. A STM is a shared object which behaves like memory that supports
    multiple changes to its addresses by means of transactions.
    12. A transaction is a thread of control which apply a finite sequence of
    primitive operations to memory.
    13. STM's correctness requirement is: every concurrent history is
    "equivalent" to some legal sequential history which is consistent with the
    real time order induced by the concurrent history.
    14. Transaction properties:
        wait-free: any process which repeatedly execute the transaction
        terminates successfully after a finite number of attemps;
        non-blocking: repeated executing some transaction by a process implies
        that some process will terminate successfully after a finite number of
        attemps in the whole system;
        swap-tolerant: non-blocking under the assumption that a process cannot
        be swaped out infinitely many times
    15. System model: i means processor ids
        current system; objects; history; real-time order; linearizability;
        Write_i(L,v): writes the value v to location L;
        Read_i(L): reads location L and return its value v;
        Load_linked_i(L): reads location L and return its value v, mark L as
        "readed by i";
        Store_conditional(L,v): if location is marked "readed by i", then write
        value v to L, and erases all existing marks by other processors on L,
        return success status, otherwise return a failure status.
    16. NOTE: definition 2.1, don't understande.
        the set of sequential histories, such that for each finite or infinite
        history h=o1o2o3..., it is the case that for all k, if ok=Tran(DataSet,
        f,r,status) and status=success then r=TS(o1o2o3..Ok-1) | DataSet.
    17. Transaction memory implementation
%{
StartTransaction(DataSet)
        Initialize(Rec[i], DataSet);
        Rec[i].stable=true;
        Transaction(Rec[i], Rec[i].version, True);
        Rec[i].stable=false;
        Rec[i].version++;
        if(Rec[i].status==Success)
                return (Success, Rec[i].OldValue);
        else
                return Failure

Transaction(rec, version, isInitiator)
        AcquireOwnerships(rec, version);
        (status, failadd)=LL(rec.status);
        if(status==Null)
                if(version != rec.version)
                        return
                SC(rec.status, (Success, 0));
        (status, failadd)=LL(rec.status);
        if(status == Success)
                AgreeOldValues(rec, version);
                NewValues=CalcNewValue(rec.OldValues);
                UpdateMemory(rec, version, NewValues);
                ReleaseOwnerships(rec, version);
        else
                ReleaseOwnerships(rec, version);
                if(isInitiator)
                        failtran=Ownerships[failadd];
                        if(failtran == Nobody)
                                return
                        else
                                failversion=failtran.version;
                                if(failtran.stable)
                                        Transaction(failtran, failversion,
                                        False);

AcquireOwnerships(rec, version)
        transize=rec.size;
        for(j=1; j<=size; j++)
                while(true)
                        location=rec.add[j]
                        if(LL(rec.status)!=Null)// before next write
                                return
                        owner=LL(Ownerships[rec.add[j])
                        if(rec.version!=version)
                                return
                        if(owner==rec)
                                exit while loop
                        if(owner==Nobody)
                                if(SC(rec.status, (Null,0)))
                                        if(SC(Ownerships[location],rec))
                                                exit while loop
                        else
                                if(SC(rec.status, (failure, j)))
                                        return

ReleaseOwnerships(rec, version)
        size=rec.size
        for(j=1;j<=size;j++)
                location=rec.add[j];
                if(LL(Ownerships[location]) == rec)
                        if(rec.version != version)
                                return;
                        SC(Ownerships[location], Nobody)

AgreeOldValues(rec, version)
        size=rec.size
        for(j=1;j<=size;j++)
                location=rec.add[j]
                if(LL(rec.oldValues[location]!=Null)) /*  ==Null ? */
                        if(rec.version != version)
                                return
                        SC(rec.oldValue[location], Memory[location])

UpdateMemory(rec, version, newvalues)
        size=rec.size
        for(j=1;j<=size;j++)
                location=rec.add[j]
                oldvalue=LL(Memory[location])
                if(rec.AllWritten)
                        return
                if(version!=rec.version)
                        return
                if(oldvalue!=newvalues[j])
                        SC(Memory[location],newvalues[j])
        if(not LL(rec.AllWritten))
                if(version!=rec.version)
                        return
                SC(rec.AllWritten, True)
}%
    18. Correctness prove
        a. An implementation based on ownership policy without helpping will
        satisfying linearizability. (We only need to prove that many processes
        executing a transaction behave just like a single process)
        b. All the processes executing a transaction perform the same
        transaction the initiator intended;
        c. All the processes agree on the final status of the transaction;
        d. The executing of a successful transaction will update memory
        correctly.
    19. Non-blocking prove
        a. No executing process will ever be able to acquire a ownership after
        the transaction has failed;
        b. Science the locations are acquired in increasing order, some
        transaction will eventually success.