Formalno verifikovana distribuirana softverska transakciona memorija otporna na otkaze

Abstract

U disertaciji je razvijena distribuirana softverska transakciona memorija u jeziku Pajton, koja je formalno verifikovana, otporna na otkaze, deterministička, i implementirana kao proširenje postojećih apstrakcija Pajtona. Ovo rešenje je namenjeno za inteligentne ugrađene sisteme na bazi Internet stvari, tj. za male i srednje ivične mreže. Prikazano rešenje se sastoji od para transakcionih koordinatora u režimu vodeći-prateći kojim upravlja distribuirani automat sa konačnim brojem stanja, i skupa servera podataka koji se ažuriraju determinističkim protokolom za replikaciju podataka. Formalna verifikacija je urađena konstruisanjem push/pull semantičkog modela i dokazivanjem odgovarajućih kriterijuma korektnosti. Eksperimentalni rezultati pokazuju super-linearno povećanje propusnosti sistema, sa promenom radnog opterećenja od opterećenja samo sa upisima ka opterećenju samo sa čitanjima.

This dissertation presents a distributed software transactional memory written in Python, which is formally verified, fault tolerant, deterministic, and implemented as an extension of the existing Python abstractions. This solution is primarily targeting intelligent embedded systems based on Internet of things, i.e. small and middle edge networks. The presented solution consists of a pair of transactional coordinators in master-slave mode controlled by a distributed finite state machine, and a set of data servers that are updated by a deterministic data replication protocol. Formal verification is made by constructing a push/pull semantic model and proving the corresponding correctness criteria. Experimental results show superlinear increase of system throughput as a workload changes from the read only to the write only.