Sharing Actors Semantics & Equivalence Analysis
Explore the semantics preservation and equivalence proofs in sharing actor systems, discussing atomicity, isolation, fairness, and state updates. An in-depth look into interaction equivalence and translation implications is provided.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Semantics-preserving Sharing Actors Mohsen Lesani{1,2} University of California, Los Angeles1 Antonio Lain2 HP Labs, Palo Alto2
Sharing Actors 2 Semantics Equivalence to Pure Actors Implementation Testing Tool
Actors 3 Actors [Hewitt][Agha] don t share state. Things in the world don't share data. [Armstrong] Race-freedom Fault-isolation Location-transparency
Sharing 4 Limited forms of sharing Efficiency Programmability What are accesses? Write-Write Multiple-Writers data Write-Read, Read-Read Single-Writer, Multiple-Readers data (SWMR data)
SWMR Data 5 Social Network Each profile is read by its friend profiles
SWMR Data with Pure Actors 6 Full Replication Delegate Actor State State State State State State Time Loss of parallelism by serializing access Time Update at each replica Space
Sharing Actors Semantics 7 Actors + SWMR State Atomicity Isolation Fairness State State State2 State2 Updates State Updates State Updates
Interaction Equivalence 8 Are two actor systems equivalent? Equivalence of the set of possible sequences of inputs and outputs Actor Semantics Sharing Actors Semantics Equivalence Proof
Translation and Equivalence 9 Sharing Actors Semantics Atomicity Isolation Fairness Actors Semantics Fairness State State State State Updates Translation State State Updates State State Updates
Translation and Equivalence 10 v+1 v State2,v State State2 State State State State2 State2 v=v ? Updates v v+1 Translation State2 State State Updates State State Updates
Sharing Actors Implementation 11 Direct (message-based) implementation of the semantics is inefficient. The optimized implementation benefits from sharing data: State State
Implementation 12 Isolation Fairness Handle Handle Head State Base Object Object Base State
Conclusion 13 Semantics-preserving Sharing Actors Sharing actors semantics Translation of sharing programs to pure programs and proof of their interaction equivalence. Implementation
Thanks for your attendance 14 Questions?
Testing Tool 15 Sharing Actors Semantics Reference Implementation Testing Tool Optimized Implementation
Testing Tool 16 Play and log with the optimized implementation (a2,n1),v1 (a2,n3),v2 Reader Reader Writer Deterministic replay with the direct implementation of the semantics (a2,n1),v1 (a2,n3),v2 Reader Reader Writer Check equality of configurations
