SOSP '25 Artifacts and Proofs - Running Consistent Applications Closer to Users with Radical for Lower Latency

Running Consistent Applications Closer to Users with Radical for Lower Latency 1 Consistency Proof 1.1 Definitions Here we show that Radical provides linearizability guarantees to its users. Linearizability is a local consistency model, thus to prove that a system is linearizable, it is sufficient to show that operations on each individual key are linearizable [ 1 ]. Without loss of generality, consider key 𝑘 . Radical supports two operations: reads ( 𝑟(𝑘𝑣) denoting that a read to key 𝑘 returns its value version 𝑣 ) and writes ( 𝑤(𝑘𝑣) denoting a write to 𝑘 of value version 𝑣 ). Linearizability requires that there exists a total order of operations on 𝑘 which we construct as follows: 1. Each write is ordered by its version number: 𝑤(𝑘𝑣)𝑒𝑥𝑒 −−→ 𝑤(𝑘𝑣+𝑖),𝑖 >0. 2. Each read is ordered after the write that it observes: 𝑤(𝑘𝑣)𝑒𝑥𝑒 −−→ 𝑟(𝑘𝑣) 3. All reads that observe the same write are ordered by invocation time: 𝑟1(𝑘𝑣)𝑒𝑥𝑒 −−→ ... 𝑒𝑥𝑒 −−→ 𝑟𝑛(𝑘𝑣) if 𝑟1.𝑖𝑛𝑣 <... < 𝑟𝑛.𝑖𝑛𝑣 For the system to be linearizable, this total order must also obey real-time ordering constraints. 1.2 Proof Thus to show that Radical is linearizable, we must show that Radical respects the above-constructed total order under real-time constraints. First, let all operation be illustrated as a directed graph where the operations are nodes that are connected by real-time edges. Then we can say that there exists a total real-time order if and only if the directed graph is acyclic (operations do not circularly affect each other), meaning that the following invariant holds: ∀𝑜𝑝𝑖, 𝑜𝑝𝑗,(𝑜𝑝𝑖 𝑟𝑡𝑜 −−→ 𝑜𝑝𝑗)=⇒ ¬(𝑜𝑝𝑗 𝑟𝑡𝑜 −−→ 𝑜𝑝𝑖). Note that there exists a real-time edge 𝑜𝑝1 𝑟𝑡𝑜 −−→ 𝑜𝑝2 if 𝑜𝑝2 sees the result of 𝑜𝑝1 and 𝑜𝑝2 starts after 𝑜𝑝1 ends ( 𝑜𝑝1.𝑟𝑒𝑠𝑝 < 𝑜𝑝2.𝑖𝑛𝑣 ). Note that this implies that operations are transitive. That is if 𝑜𝑝1 𝑟𝑡𝑜 −−→ 𝑜𝑝2 and 𝑜𝑝2 𝑟𝑡𝑜 −−→ 𝑜𝑝3 , then 𝑜𝑝1 𝑟𝑡𝑜 −−→ 𝑜𝑝3 . Two operations have a real-time edge in one of two cases: 1. 𝑜𝑝1 and 𝑜𝑝2 are performed sequentially by the same function execution where 𝑜𝑝1precedes 𝑜𝑝2 2. 𝑜𝑝1 and 𝑜𝑝2 are performed by two different executions, and 𝑜𝑝2sees the result of 𝑜𝑝1via Radical’s design We prove that Radical’s total order is a real-time order by contradiction. More specifically, we consider pairs of operations (𝑤,𝑤),(𝑟,𝑟),(𝑟, 𝑤),(𝑤, 𝑟). 1. (𝑤,𝑤) :let there be two writes such that 𝑤1=𝑤(𝑘𝑣)𝑒𝑥𝑒 −−→ 𝑤2=𝑤(𝑘𝑣′), 𝑣′>𝑣 . By the contradiction we assume we also have 𝑤2 𝑟𝑡𝑜 −−→ 𝑤1 . Because 𝑤2 is real-time ordered before another operation, we know 𝑤2 must have completed. There are two cases: a. 𝑤2 completed at the edge. Then it must have acquired a write lock as part of its successful consistency check (lines XX–YY). This lock precludes any other operation from acquiring a write lock (lines XX–YY) until it is released. There are three subcases depending on how 𝑤1executes: i. 𝑤1 completes at the edge. Then it must also acquire a write lock as part of its successful consistency check. Since 𝑤2 𝑟𝑡𝑜 −−→ 𝑤1 , then 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑤2.𝑟𝑒𝑠𝑝 <𝑤1.𝑖𝑛𝑣 <𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 , so we know that 𝑤1 must acquire its lock after 𝑤2 releases its lock. Version numbers only increase for subsequent writes (lines XX–YY), so 𝑣′ (written by 𝑤2 ) <𝑣(written by 𝑤1). Contradiction. ii. 𝑤1 completes in the datacenter. Then it must also acquire a write lock as part of its failed consistency check. 𝑤2 must have released the locks before 𝑤1 could start running at the datacenter, so if 𝑤2 𝑟𝑡𝑜 −−→ 𝑤1 , then 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑤2.𝑟𝑒𝑠𝑝 < 𝑤1.𝑖𝑛𝑣 <𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 , similarly to the case when 𝑤1 completes in the edge. Version numbers only increase for subsequent writes, so 𝑣′<𝑣 . Contradiction. iii. 𝑤2 completes at the datacenter or at the edge as part of a timeout. If 𝑤2 started running at the edge, then it must have acquired a write lock as part of its consistency check. If the datacenter times out on the follow-up from the edge, the write lock is still held, and the execution is rerun in the datacenter. Thus, depending on whether the follow-up from the edge finally arrives or the function on the datacenter finishes executing first, the same logic from cases (i) and (ii) applies. If the function finished executing first, the later stale follow-up is discarded, and if the follow-up arrives during datacenter execution, the result of the datacenter execution is ignored. b. 𝑤2 completes in the datacenter. Then it must have acquired a write lock as part of its failed consistency check (lines XX-YY). No other operations, whether in the datacenter or at the edge, could be performing operations on 𝑘 until 𝑤2 completes. There are two 1 subcases depending on where 𝑤1 executes (we omit the timeout case as the reasoning is similar to what is described in 1(a)iii): i. 𝑤1 completes at the edge. Then it must have been the case that 𝑤1 acquired the write lock as part of its successful consistency check. This necessitates that 𝑤2 released its lock first. If 𝑤2 𝑟𝑡𝑜 −−→ 𝑤1 , then 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑤2.𝑟𝑒𝑠𝑝 <𝑤1.𝑖𝑛𝑣 < 𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 . Version numbers only increase for subsequent writes, so 𝑣′<𝑣. Contradiction. ii. 𝑤1 completes at the datacenter. Then it must have waited for 𝑤2 to release its lock before acquiring the lock as part of its failed consistency check. Thus, 𝑤2 and 𝑤1 execute at the datacenter sequentially, in that order. As in the above case, 𝑤2 𝑟𝑡𝑜 −−→ 𝑤1=⇒𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑤2.𝑟𝑒𝑠𝑝 < 𝑤1.𝑖𝑛𝑣 <𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 , and since version numbers only increase for subsequent writes, so 𝑣′<𝑣 . Contradiction. 2. (𝑟,𝑟) :let there be two reads such that 𝑟1 𝑒𝑥𝑒 −−→ 𝑟2 . By the contradiction we assume we also have 𝑟2 𝑟𝑡𝑜 −−→ 𝑟1 . Because 𝑟2 is real-time ordered before another operation, we know 𝑟2must have completed. There are two cases: a. If 𝑟1=𝑟(𝑘𝑣) and 𝑟2=𝑟(𝑘𝑣) return the same values, then the two reads are ordered by invocation time. Since 𝑟1.𝑖𝑛𝑣 <𝑟2.𝑖𝑛𝑣 , there cannot be a real-time edge from 𝑟2to 𝑟1. Contradiction. b. If 𝑟1=𝑟(𝑘𝑣) and 𝑟2=𝑟(𝑘𝑣′) where 𝑣′>𝑣 and 𝑟1 𝑒𝑥𝑒 −−→ 𝑟2 , then there must exist 𝑤1 that 𝑟1 sees and 𝑤2 that 𝑟2 sees, such that 𝑤2 is ordered after 𝑤1 . In other words, it must be the case that 𝑤1 𝑒𝑥𝑒 −−→ 𝑟1 , 𝑤2 𝑒𝑥𝑒 −−→ 𝑟2 , and 𝑤1 𝑒𝑥𝑒 −−→ 𝑤2 . Assuming there exists the edge 𝑟2 𝑟𝑡𝑜 −−→ 𝑟1 , then we know that 𝑟2 must have completed. There are two cases: i. If 𝑟2 completed at the edge, it must be the case that the read lock on 𝑘 was acquired and the consistency check was successful. Thus, there could have been no writes to 𝑘 between 𝑟2.𝑖𝑛𝑣 and 𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . There are two subcases depending on where 𝑟1executes: A. 𝑟1 also completes at the edge. Then it must have also acquired a read lock on 𝑘 to ensure all pending writes were complete. However, 𝑟1 would have acquired the read lock after 𝑤1 executed. Since 𝑤1 should have acquired a write lock before 𝑟1 , it is necessary that 𝑤1 executed between 𝑟2.𝑟𝑒𝑎𝑑_𝑢𝑛𝑙𝑜𝑐𝑘 and 𝑟1.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . In other words, the following must be true: 𝑟2.𝑖𝑛𝑣 <𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 <𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑟1.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . Since 𝑟2.𝑟𝑒𝑠𝑝 <𝑟1.𝑖𝑛𝑣 by assumption ( 𝑟2 𝑟𝑡𝑜 −−→ 𝑟1 ) and 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 ( 𝑤2 𝑒𝑥𝑒 −−→ 𝑟2 ), then transitively, it must be true that 𝑤2 𝑟𝑡𝑜 −−→ 𝑟1 . Since reads must be ordered after the writes they observe, 𝑤1 must occur between 𝑤2 and 𝑟1 . However, writes are ordered in increasing version number in the total order, and since 𝑤2=𝑤(𝑘𝑣′),𝑤1= 𝑤(𝑘𝑣), 𝑣′>𝑣, this is a contradiction. B. 𝑟1 completes at the datacenter. Then it must have acquired a read lock on 𝑘 to avoid reading stale data. Similarly, 𝑤1 must have acquired the write lock at some point before 𝑟1 acquired its read lock. Similar to the above, we necessarily expect that 𝑟2.𝑖𝑛𝑣 <𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 < 𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑟1.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 and 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . Thus 𝑤2 𝑟𝑡𝑜 −−→ 𝑟1=⇒𝑤2 𝑒𝑥𝑒 −−→ 𝑤1 𝑒𝑥𝑒 −−→ 𝑟1 which violates legal ordering of writes by version number. Contradiction. ii. If 𝑟2 completed at the datacenter, then the read lock on 𝑘 was acquired as part of a failed consistency check. No executions that write to 𝑘 are possible (whether at datacenter or on edge) once the read lock is acquired. As described above, regardless of where 𝑟1 executes, 𝑤1 must have obtained a write lock beforehand such that 𝑤2.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑟2.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 <𝑤1.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑟1.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . Consequently, 𝑤2 𝑟𝑡𝑜 −−→ 𝑟1 , 𝑤2 𝑒𝑥𝑒 −−→ 𝑤1 𝑒𝑥𝑒 −−→ 𝑟1 which is out of order writes. Contradiction. 3. (𝑟,𝑤) :let there be a read and a write such that 𝑟=𝑟(𝑘𝑣)𝑒𝑥𝑒 −−→ 𝑤′=𝑤(𝑘𝑣′), 𝑣′>𝑣 . By the contradiction we also have 𝑤′𝑟𝑡𝑜 −−→ 𝑟 . Because 𝑤′ is real-time ordered before another operation, we know 𝑤′ must have completed. There are two cases: a. 𝑤′ completes at the edge. Then it must have acquired a write lock on 𝑘 before 𝑟 executed. Whether 𝑟 was executed on edge or in datacenter, it held the read lock and sent a response back to the user before 𝑤′ took its write lock. In other words, since 𝑤′𝑟𝑡𝑜 −−→ 𝑟 , then 𝑤′.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑤′.𝑟𝑒𝑠𝑝 <𝑟.𝑖𝑛𝑣 <𝑟.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 . However, 𝑟 would return the value of 𝑘 of version 𝑣 , not 𝑣′ . Thus there must exist a write 𝑤=𝑤(𝑘𝑣) that is ordered between 𝑤′ and 𝑟 such that 𝑤′𝑒𝑥𝑒 −−→ 𝑤𝑟 −→ , which are out-of-order writes. Contradiction. b. 𝑤′ completed at the datacenter. Then it must have acquired a write lock as part of its failed consistency check. Then 𝑤 , by the same logic as above, either executes in datacenter or on edge, after 𝑤′ released its lock, so if 𝑤′𝑟𝑡𝑜 −−→ 𝑟 , the operations must be ordered as 𝑤′𝑒𝑥𝑒 −−→ 𝑤𝑟 −→ , guaranteed by 𝑤′.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 < 𝑤.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 <𝑟.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 , which are out-of-order writes. Contradiction. 2 4. (𝑤, 𝑟) :let there be a write and a read that observes that write such that 𝑤=𝑤(𝑘𝑣)𝑒𝑥𝑒 −−→ 𝑟=𝑟(𝑘𝑣) . By the contradiction we also have 𝑟𝑟𝑡𝑜 −−→ 𝑤 . Because 𝑟 is real-time ordered before another operation, we know 𝑟 must have completed. There are two cases: a. 𝑟 completes at the edge. Then it must have acquired a read lock on 𝑘 . There are then two subcases on where 𝑤is executed: i. If 𝑤 is executed on the edge, then it acquired the write lock and necessarily after 𝑟 released its read lock. Thus 𝑟 must have read some data before 𝑤 executed. Since 𝑟 read 𝑘𝑣 before 𝑘𝑣 was written by 𝑤 , the read is not ordered by the write it observes. Contradiction. ii. If 𝑤 executed in the datacenter, then similarly 𝑟.𝑖𝑛𝑣 <𝑟.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 <𝑟.𝑟𝑒𝑠𝑝 <𝑤.𝑖𝑛𝑣 <𝑤.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 which means that the read is not ordered after the write it observes. Contradiction. b. 𝑟 completes at the datacenter as a result of a failed consistency check. It does so after acquiring a read lock such that all pending writes complete first. Consider where 𝑤is executed afterwards: i. If 𝑤 is executed at the edge, then 𝑤 acquired a write lock as part of a successful consistency check, thereby requiring that 𝑟.𝑟𝑒𝑎𝑑_𝑙𝑜𝑐𝑘 <𝑤.𝑤𝑟𝑖𝑡𝑒_𝑙𝑜𝑐𝑘 . The write lock is only released upon central datastore update as a result of the follow up from edge. Thus if 𝑟𝑟𝑡𝑜 −−→ 𝑤 , then the read would observe a write that did not yet occur. Contradiction. ii. If and when 𝑤 is executed at the datacenter, then 𝑟 must have already released its read lock. In other words, 𝑟 and 𝑤 are executed sequentially at the datacenter, so the read would not be ordered after the write it observes. Contradiction. Thus, the ordering obeys the real-time order for all pairs of operations on each key 𝑘 . Because our given ordering is a legal total order that obeys real-time constraints, Radical provides linearizability. References [1] Maurice P Herlihy and Jeannette M Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463–492, 1990. 3