National Repository of Dissertations in Serbia
    • English
    • Српски
    • Српски (Serbia)
  • English 
    • English
    • Serbian (Cyrilic)
    • Serbian (Latin)
  • Login
View Item 
  •   NaRDuS home
  • Универзитет у Новом Саду
  • Факултет техничких наука
  • View Item
  •   NaRDuS home
  • Универзитет у Новом Саду
  • Факултет техничких наука
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Formalno verifikovana distribuirana softverska transakciona memorija otporna na otkaze

Formally verified fault tolerant distributed software transactional memory

Thumbnail
2021
Disertacija.pdf (2.653Mb)
IzvestajKomisije.pdf (379.1Kb)
Author
Popović Marko
Mentor
Bašičević, Ilija
Committee members
Teslić, Nikola
Tomašević Milo
Gilezan, Silvia
Đukić, Miodrag
Bašičević, Ilija
Metadata
Show full item record
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.
Faculty:
Универзитет у Новом Саду, Факултет техничких наука
Date:
09-04-2021
Keywords:
distribuirana transakciona memorija / distributed transactional memory / formalna verifikacija / otpornost na otkaze / determinizam / replikacija podataka / Pajton / formal verification / fault tolerance,determinism / data replication / Python
[ Google Scholar ]
Handle
https://hdl.handle.net/21.15107/rcub_nardus_18373
URI
http://www.cris.uns.ac.rs/DownloadFileServlet/Disertacija161104932670295.pdf?controlNumber=(BISIS)117485&fileName=161104932670295.pdf&id=17440&source=NaRDuS&language=sr
http://www.cris.uns.ac.rs/record.jsf?recordId=117485&source=NaRDuS&language=sr
http://www.cris.uns.ac.rs/DownloadFileServlet/IzvestajKomisije16110493909367.pdf?controlNumber=(BISIS)117485&fileName=16110493909367.pdf&id=17441&source=NaRDuS&language=sr
/DownloadFileServlet/IzvestajKomisije16110493909367.pdf?controlNumber=(BISIS)117485&fileName=16110493909367.pdf&id=17441
https://nardus.mpn.gov.rs/handle/123456789/18373

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS
 

 

Browse

All of DSpaceUniversities & FacultiesAuthorsMentorCommittee membersSubjectsThis CollectionAuthorsMentorCommittee membersSubjects

DSpace software copyright © 2002-2015  DuraSpace
About NaRDus | Contact us

OpenAIRERCUBRODOSTEMPUS