mutex.ivy

#lang ivy1.7

################################################################################
# A liveness proof of a futex-based mutex
################################################################################


################################################################################
#
# Types, relations and functions describing the state
#
################################################################################


isolate mutex_protocol = {

    type thread

    action step_atomic_cas(t:thread)
    action step_futex_wait(t:thread)
    action step_kernel_wait(t:thread)
    action step_atomic_store(t:thread)
    action step_futex_wake(t:thread)
    action step_finished(t:thread)
    action add_to_d(t:thread)

    specification {

    # global state (lock and futex queue)
    relation locked
    relation queue(T:thread)

    # local state (program counters)
    relation pc_atomic_cas(T:thread)
    relation pc_futex_wait(T:thread)
    relation pc_kernel_wait(T:thread)
    relation pc_atomic_store(T:thread)
    relation pc_futex_wake(T:thread)
    relation pc_finished(T:thread)

    # for tracking fairness assumptions
	relation scheduled(T:thread)

	after init {
            pc_atomic_cas(T) := true;
            pc_futex_wait(T) := false;
            pc_kernel_wait(T) := false;
            pc_atomic_store(T) := false;
            pc_futex_wake(T) := false;
            pc_finished(T) := false;
            locked := false;
            queue(T) := false;
            scheduled(T) := false;
	}

	before step_atomic_cas {
        require pc_atomic_cas(t);
        pc_atomic_cas(t) := false;
        if locked {
            pc_futex_wait(t) := true;
        } else {
            # successfully acquired the lock
            pc_atomic_store(t) := true;
            locked := true;
        }
        scheduled(T) := T = t;
	    scheduled(T) := false;
	}

    before step_futex_wait {
        require pc_futex_wait(t);
        pc_futex_wait(t) := false;
        if locked {
            # start waiting in kernel
            pc_kernel_wait(t) := true;
            queue(t) := true;
        } else {
            pc_atomic_cas(t) := true;
        }
        scheduled(T) := T = t;
        scheduled(T) := false;
    }

    before step_kernel_wait {
        require pc_kernel_wait(t);
        if ~queue(t) {
            pc_kernel_wait(t) := false;
            pc_atomic_cas(t) := true;
        }
        scheduled(T) := T = t;
        scheduled(T) := false;
    }

    before step_atomic_store {
        require pc_atomic_store(t);
        pc_atomic_store(t) := false;
        pc_futex_wake(t) := true;
        locked := false;
        scheduled(T) := T = t;
        scheduled(T) := false;
    }

    before step_futex_wake {
        require pc_futex_wake(t);
        pc_futex_wake(t) := false;
        if some t_q:thread. queue(t_q) {
            queue(t_q) := false;
        } # otherwise no signalling is needed
        pc_finished(t) := true;
        scheduled(T) := T = t;
        scheduled(T) := false;
    }

    before step_finished {
        require pc_finished(t);
        scheduled(T) := T = t;
        scheduled(T) := false;
    }

	################################################################################
	#
	# Invariants for proving safety (also help for liveness)
	#
	################################################################################

	# basic

    invariant pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T) | pc_atomic_store(T) | pc_futex_wake(T) | pc_finished(T)
    invariant ~pc_atomic_cas(T) | ~pc_futex_wait(T)
    invariant ~pc_atomic_cas(T) | ~pc_kernel_wait(T)
    invariant ~pc_atomic_cas(T) | ~pc_atomic_store(T)
    invariant ~pc_atomic_cas(T) | ~pc_futex_wake(T)
    invariant ~pc_atomic_cas(T) | ~pc_finished(T)
    invariant ~pc_futex_wait(T) | ~pc_kernel_wait(T)
    invariant ~pc_futex_wait(T) | ~pc_atomic_store(T)
    invariant ~pc_futex_wait(T) | ~pc_futex_wake(T)
    invariant ~pc_futex_wait(T) | ~pc_finished(T)
    invariant ~pc_kernel_wait(T) | ~pc_atomic_store(T)
    invariant ~pc_kernel_wait(T) | ~pc_futex_wake(T)
    invariant ~pc_kernel_wait(T) | ~pc_finished(T)
    invariant ~pc_atomic_store(T) | ~pc_futex_wake(T)
    invariant ~pc_atomic_store(T) | ~pc_finished(T)
    invariant ~pc_futex_wake(T) | ~pc_finished(T)

    #######################################
    # Safety invariant (mutual exclusion)
    #######################################
	invariant pc_atomic_store(T1) & pc_atomic_store(T2) -> T1 = T2

	# inductive invariant for proving safety
    invariant pc_atomic_store(T) -> locked

        ################################################################################
	#
	# Temporal property and its proof
	#
	################################################################################

    # workaround to take advantage of the fact that the set of threads is finite
    #
    # d will accumulate threads one step at a time, and we'll assume eventually,
    # forall T. d(T). This makes sense when `thread` is a finite type, which is
    # a consistent thing to assume.
    relation d(T:thread)
    after init {
        d(T) := false;
    }
    before add_to_d { d(t) := true }
    # fairness: eventually forall T. d(T)

    individual t0:thread  # witness for the formula (exists T0. (globally ~(pc_finished(T0))))

	temporal property [nonstarvation] (
            # temporal witnesses
            (exists T0. (globally ~pc_finished(T0))) -> (globally ~(pc_finished(t0))) &
            # finitely many threads
            eventually forall T. d(T)
        ) -> (
            # temporal property
            (forall T. globally (eventually scheduled(T))) -> (forall T. eventually (pc_finished(T)))
        )
    proof {
            tactic l2s with

	        invariant ~scheduled(T)  # scheduled is only true transiently inside actions

            # basic, should be added automatically
            invariant l2s_waiting | l2s_frozen | l2s_saved
            invariant ~l2s_waiting | ~l2s_frozen
            invariant ~l2s_waiting | ~l2s_saved
            invariant ~l2s_frozen  | ~l2s_saved

            # safety invariants for saved copy
            invariant l2s_saved -> (
            ($l2s_s T. pc_atomic_cas(T))(T) | ($l2s_s T. pc_futex_wait(T))(T) | ($l2s_s T. pc_kernel_wait(T))(T) | ($l2s_s T. pc_atomic_store(T))(T) | ($l2s_s T. pc_futex_wake(T))(T) | ($l2s_s T. pc_finished(T))(T)
            )

            invariant l2s_saved -> (~($l2s_s T. pc_atomic_cas(T))(T) | ~($l2s_s T. pc_futex_wait(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_cas(T))(T) | ~($l2s_s T. pc_kernel_wait(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_cas(T))(T) | ~($l2s_s T. pc_atomic_store(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_cas(T))(T) | ~($l2s_s T. pc_futex_wake(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_cas(T))(T) | ~($l2s_s T. pc_finished(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_futex_wait(T))(T) | ~($l2s_s T. pc_kernel_wait(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_futex_wait(T))(T) | ~($l2s_s T. pc_atomic_store(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_futex_wait(T))(T) | ~($l2s_s T. pc_futex_wake(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_futex_wait(T))(T) | ~($l2s_s T. pc_finished(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_kernel_wait(T))(T) | ~($l2s_s T. pc_atomic_store(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_kernel_wait(T))(T) | ~($l2s_s T. pc_futex_wake(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_kernel_wait(T))(T) | ~($l2s_s T. pc_finished(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_store(T))(T) | ~($l2s_s T. pc_futex_wake(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_atomic_store(T))(T) | ~($l2s_s T. pc_finished(T))(T))
            invariant l2s_saved -> (~($l2s_s T. pc_futex_wake(T))(T) | ~($l2s_s T. pc_finished(T))(T))

            # safety property
            invariant l2s_saved -> (($l2s_s T. pc_atomic_store(T))(T1) & ($l2s_s T. pc_atomic_store(T))(T2) -> T1 = T2)

            # inductive invariant for proving safety
            invariant l2s_saved -> (($l2s_s T. pc_atomic_store(T))(T) -> ($l2s_s. locked))


            # basic temporal information from temporal property
            invariant globally eventually scheduled(T)
            invariant globally (~pc_finished(t0))
            invariant ~pc_finished(t0)

            # finite-thread workaround
            #
            # l2s_d is the finite abstraction of the system, and because of
            # finiteness it can contain every thread.
            invariant eventually forall T. d(T)
            invariant ($l2s_w. forall T. d(T)) | forall T. d(T)
            invariant d(T) -> l2s_d(T)
            invariant (l2s_frozen | l2s_saved) -> forall T:thread. l2s_d(T)
            invariant (l2s_frozen | l2s_saved) -> forall T:thread. l2s_a(T)

            # if a thread is waiting to be scheduled, its PC won't change
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_atomic_cas(T))(T) <-> pc_atomic_cas(T))
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_futex_wait(T))(T) <-> pc_futex_wait(T))
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_kernel_wait(T))(T) <-> pc_kernel_wait(T))
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_atomic_store(T))(T) <-> pc_atomic_store(T))
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_futex_wake(T))(T) <-> pc_futex_wake(T))
            invariant l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc_finished(T))(T) <-> pc_finished(T))

            # a simple invariant from the fact that entering kernel_wait is the
            # only way to enter the queue
            invariant queue(T) -> pc_kernel_wait(T)
            invariant l2s_saved -> (($l2s_s T. queue(T))(T) -> ($l2s_s T. pc_kernel_wait(T))(T))

            # threads in unlock make monotonic progress
            invariant [atomic_store_progress] l2s_saved -> (
              ($l2s_s T. pc_atomic_store(T))(T) & ~($l2s_w T. scheduled(T))(T) ->
              (pc_futex_wake(T) | pc_finished(T))
            )
            invariant [futex_wake_progress] l2s_saved -> (
              ($l2s_s T. pc_futex_wake(T))(T) & ~($l2s_w T. scheduled(T))(T) ->
              pc_finished(T)
            )
            invariant [finished_stable] l2s_saved -> (
              ($l2s_s T. pc_finished(T))(T) ->
              pc_finished(T)
            )

            # if the lock is held, then there's a thread in atomic_store and the
            # above argument shows that it must make progress when scheduled
            invariant [locked_thread] locked -> exists T. pc_atomic_store(T)

            # A key invariant of the liveness proof: if a thread is in
            # kernel_wait, in the queue (therefore not enabled), and the lock is
            # free (thus the above argument doesn't apply), then there exists a
            # thread in futex_wake or atomic_cas. This is the thread that will
            # make progress.
            invariant [kernel_wait_exist] forall T1. pc_kernel_wait(T1) & queue(T1) & ~locked -> (
                exists T2. pc_futex_wake(T2) | pc_atomic_cas(T2) |
                (pc_kernel_wait(T2) & ~queue(T2))
            )
            #invariant l2s_saved -> forall T1. ($l2s_s T. pc_kernel_wait(T))(T1) -> (
            #    exists T2. ($l2s_s T. pc_futex_wake(T))(T2) | ($l2s_s T. pc_atomic_store(T))(T2) | ($l2s_s T. pc_atomic_cas(T))(T2) |
            #    (($l2s_s T. pc_kernel_wait(T))(T2) & ~($l2s_s T. queue(T))(T2))
            #)
            #invariant l2s_saved -> forall T1. (
            #~($l2s_s. locked) & ($l2s_s T. pc_kernel_wait(T))(T1) & ~($l2s_s T. queue(T))(T1) &
            #~($l2s_w T. scheduled(T))(T1)
            #) -> (
            #pc_atomic_cas(T1) |
            #exists T2. (($l2s_s T. pc_atomic_cas(T))(T2) |
            #        ($l2s_s T. pc_futex_wait(T))(T2) |
            #        ($l2s_s T. pc_kernel_wait(T))(T2)) &
            #        (pc_atomic_store(T2) |
            #         pc_futex_wake(T2) |
            #         pc_finished(T2))
            #)

            ## ------------------
            ## We'll now have several invariants with the same premise: the lock
            ## was free in the saved state and every thread in the lock() code
            ## is still there. If the lock was held, then the above arguments
            ## show that the thread holding the lock would have changed. If some
            ## thread in lock ended up not in the lock, then that represents a
            ## change and thus this isn't a loop.
            ##
            ## What we need to show is that it's not possible for a thread in
            ## the lock() code in the saved state to be in exactly the same
            ## state now. As long as there's some change, then this execution
            ## isn't a loop and thus isn't a counter-example to liveness.
            ## ------------------

            # if the lock was free and a thread was in lock and is still in
            # lock, then the lock is still free
            invariant l2s_saved -> (
            (~($l2s_s. locked) &
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) |
                ($l2s_s T. pc_futex_wait(T))(T) |
                ($l2s_s T. pc_kernel_wait(T))(T)) ->
            (pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T)))) ->
            ~locked
            )

            # under these conditions, there can't be a scheduled thread in
            # atomic_cas in the saved state (since it would have acquired the
            # lock)
            invariant [atomic_cas_progress] l2s_saved -> (
            (~($l2s_s. locked) &
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) |
                ($l2s_s T. pc_futex_wait(T))(T) |
                ($l2s_s T. pc_kernel_wait(T))(T)) ->
            (pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T)))) ->
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) &
                 ~($l2s_w T. scheduled(T))(T)) ->
                false
            )
            )

            # a thread in futex_wait would have moved to atomic_cas, which is a
            # change and thus this isn't a loop
            invariant [futex_wait_progress] l2s_saved -> (
            (~($l2s_s. locked) &
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) |
                ($l2s_s T. pc_futex_wait(T))(T) |
                ($l2s_s T. pc_kernel_wait(T))(T)) ->
            (pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T)))) ->
            (forall T.
                (($l2s_s T. pc_futex_wait(T))(T) &
                 ~($l2s_w T. scheduled(T))(T)) ->
                pc_atomic_cas(T)
            )
            )

            # a thread in kernel_wait but not in the queue is enabled and must
            # have moved to atomic_cas (because the assumption is that it stayed
            # in lock()), which is a change
            invariant [kernel_wait_unqueued] l2s_saved -> (
            (~($l2s_s. locked) &
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) |
                ($l2s_s T. pc_futex_wait(T))(T) |
                ($l2s_s T. pc_kernel_wait(T))(T)) ->
            (pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T)))) ->
            (forall T.
                (($l2s_s T. pc_kernel_wait(T))(T) &
                 ~($l2s_s T. queue(T))(T) &
                 ~($l2s_w T. scheduled(T))(T)) ->
                pc_atomic_cas(T)
            )
            )

            # For the above argument to hold inductively, we need to show that a
            # thread not in the queue stays out of the queue. This is true
            # because the futex_wait -> kernel_wait transition that adds to the
            # queue requires the lock to be held, and it can't do that in these
            # circumstances.
            #
            # NOTE(tej): not sure I can concretely explain why this is useful
            invariant l2s_saved -> (
            (~($l2s_s. locked) &
            (forall T.
                (($l2s_s T. pc_atomic_cas(T))(T) |
                ($l2s_s T. pc_futex_wait(T))(T) |
                ($l2s_s T. pc_kernel_wait(T))(T)) ->
            (pc_atomic_cas(T) | pc_futex_wait(T) | pc_kernel_wait(T)))) ->
            (forall T.
                (~($l2s_s T. queue(T))(T)) ->
                ~queue(T)
            )
            )

            # The final case is that a thread was in kernel_wait and was in the
            # queue; the invariant `kernel_wait_exist` above shows that then
            # there's some other thread that will change state if schedule
            # (either a futex_wake that will transition to finished, or an
            # atomic_cas that can't stay in lock() as we assumed).

    }
}
}

export mutex_protocol.step_atomic_cas
export mutex_protocol.step_futex_wait
export mutex_protocol.step_kernel_wait
export mutex_protocol.step_atomic_store
export mutex_protocol.step_futex_wake
export mutex_protocol.step_finished
export mutex_protocol.add_to_d