proof.md

There are three steps to the locking operation, the lock step (which we will refer to as lock()), the execution actual payout function (payout()), followed by the lock release (release()). We assume that all of these functions will return true if and only if the action succeeded. Specifically, we assume that lock() will return false if the atomic database operation did not modify the document and will return true when the document has been modified and the modification has been fully propagated. These are guarantees provided by MongoDB's atomic update operation (source: https://pymongo.readthedocs.io/en/stable/api/pymongo/results.html#pymongo.results.UpdateResult) and by mongodb_dataset's update result checks.

Given the lock only has two states, locked or unlocked, and if it is unlocked, lock() will succeed, lock() can only return false if the file is already locked.

This is the pseudo structure of both programs:

worker 1 (w_1):

if lock_status_1 := lock():
    payout()
    lock_status_1 = False
    release()

worker 2 (w_2):

if lock_status_2 := lock():
    payout()
    lock_status_2 = False
    release()

For the purposes of the proof, line 3 in both programs have been added. In our system model, time and order of operations is considered from the database's perspective (MongoDB actions are monotonic: https://docs.mongodb.com/manual/core/read-isolation-consistency-recency/#causal-consistency-guarantees).

Suppose that two workers are executing payout() concurrently. For this to occur, lock_status_1 and lock_status_2 need to be true at the same time since lock_status_1 and lock_status_2 must both be true for the duration of the execution of payout(). Without loss of generality, assume w_2 is executed sometime after w_1. Either w_2 is executed before or after w_1's execution of release().

If it is executed before release(), then calling lock() will not modify the MongoDB document and will return False. =><=

If it is executed after release(), then payout() has finished executing in w_1 and two workers are not executing payout() concurrently. =><=

Therefore, the two workers cannot execute payout() concurrently.

Qed.