Semantics-preserving Sharing Actors

Actors interact by asynchronous message passing. A key semantic property of actors is that they do not share state. This facilitates data-race freedom, fault isolation and location transparency. On the other hand, strict avoidance of sharing can lead to inefficiency. We propose the sharing actor programming model that extends the actor programming model with single-writer multiple-reader sharing of data. We define the sharing actor theory and prove its semantic equivalence to the pure actor theory. We realize the sharing actor theory with an efficient implementation. The implementation benefits from sharing data but keeps it transparent to actors. To increase the confidence that the implementation complies with the semantics, we have built a checking tool based on deterministic replay of actor programs