Linearizability of Construction-Then-Read: Eliminating Partial Initialization (NuSMV)

Description of the Case Study

This case study models an object that is constructed by one thread and observed by another. A constructor thread emits a construction-begun event and then writes two object fields in program order. A listener thread, after observing the event, reads both fields and produces return values derived from those reads. A “bad read” denotes any execution in which the listener has observed the construction event yet still reads a default (uninitialized) value from at least one field, reflecting a partially initialized state. The concurrent realization permits arbitrary interleavings between the constructor and listener, making such partial observations possible. The sequential reference realization delays the listener until construction has completed, ensuring that both reads observe initialized values and preventing bad reads. The linearizability requirement is that every behavior of the concurrent realization correspond to some behavior of the sequential reference with identical listener outcomes, which rules out executions exhibiting bad reads.

The NuSMV model(s)

ConcurrentSequential

MODULE main
    VAR 
        --Constructor Thread Vars
        constructorMem : 0..1; -- (0 = Uninitialized, 1 = Set)
        x : 0..1; -- (0 = Uninit, 1 = Set)
        y : 0..1; -- (0 = Uninit, 1 = Set)
        constructorClock : 0..4; -- (represents stalling the constructor process)
        constructorPC : 0..3; -- (represented position in program for constructor)
        constructorThreadStatus : 0..1; -- (0 = Dead, 1 = Alive)

            --ReaderFunctionvariables
        i : 0..2;
        j : 0..2;

        --Listener Thread vars
        --x : 0..1; -- 
        listenerClock : 0..2;
        listenerPC : 0..5;
        listenerEvent : 0..1;

        --Event

    ASSIGN
        -- Initialize
        --  Constructor State
        
        init(constructorClock) := {1, 2}; -- How long the process will have to wait to perform its action.
        init(constructorPC) := 0;
        
        init(x) := 0;
        init(y) := 0;
        init(i) := 0; 
        init(j) := 0;

        -- Driver / Listener State
        
        init(listenerClock) := 0; -- How long the process will have to wait to perform its action.
        init(listenerPC) := 0;
        init(constructorThreadStatus) := 0; -- Constructor call simluation
        init(listenerEvent) := {0, 1};


        --Constructor Transitions
        next(constructorPC) := case
            constructorPC < 3 & constructorClock = 0: constructorPC + 1;
            TRUE : constructorPC;
        esac; 

        next(constructorClock) := case
            constructorThreadStatus = 0 : constructorClock;
            constructorClock > 0 : constructorClock - 1;
            TRUE : {1, 2};
        esac;

        
        next(constructorMem) := case
            constructorClock = 0 & constructorPC = 0 : 1; -- mem init
            TRUE : constructorMem;
        esac;

        next(x) := case
            constructorClock = 0 & constructorPC = 1 : 1; --Set x if the program is at that line
            TRUE : x; --Set
        esac;

        next(y) := case
            constructorClock = 0 & constructorPC = 2 : 1; --Set y if the program is at that line
            TRUE : y; --stay
        esac;

        next(i) := case
            constructorMem != 0 & listenerPC = 4 : x + 1;     -- Read the value of x into the i var if in the correct spot in the listener program and constructor is init
            TRUE : i;
        esac;
        
        next(j) := case
            constructorMem != 0 & listenerPC = 5 : y + 1;     -- Read the value of y into the j var if in the correct spot in the listener program and constructor is init
            TRUE : j;
        esac;

        -- Listener transitions


        next(listenerClock) := case
            listenerClock > 0 : listenerClock - 1;
            TRUE : {0, 1};
        esac;

        next(listenerPC) := case
            listenerClock = 0 & (listenerPC < 3 | listenerPC = 4) : listenerPC + 1; --linear ticking
            listenerClock = 0 & listenerPC = 3 : {3, 4}; --listen for event, move on if it happened
            listenerClock = 0 & listenerPC = 5 : 3; -- go back to listening
            TRUE: listenerPC;
        esac;

        next(constructorThreadStatus) := case
            listenerPC = 1 : 1; --first thing the listener PC does is start the constructor
            constructorPC = 3 : 0; --kill thread when constructor complete
            TRUE : constructorThreadStatus;
        esac;

        DEFINE
            READVALUE := (i !=0 & j != 0);
            BADREAD := (i = 1 | j = 1);

The HyperLTL formula

Linearizability here requires that every concurrent execution of the construction-then-read scenario be observationally equivalent to a sequential execution in which the constructor’s writes take effect at a single atomic point between its invocation and completion, prior to the listener’s reads. When this property holds, it shows that the listener can never return values reflecting a partially initialized object, thereby ruling out bad reads and providing evidence that construction and memory-visibility semantics are correct under all thread interleavings.

\[\varphi_{\text{lin}} = \forall \pi_A.\exists \pi_B.\ \Box\left( \mathit{history}_{\pi_A} \leftrightarrow \mathit{history}_{\pi_B} \right)\]

Case Constructor

Forall A . Exists B . G((i[A] = i[B]) & (j[A] = j[B]))

References