Distributed applications often deal with data with different consistency requirements: while a post in a social network only requires weak consistency, the user balance in turn has strong correctness requirements, demanding mutations to be synchronised. To deal efficiently with sequences of operations on different replicas of the distributed application, it is useful to know which operations commute with others and thus, when can an operation not requiring synchronisation be anticipated wrt other requiring it, thus avoiding unnecessary waits. Herein we present a language-based static analysis to extract at compile-time from code information on which operations can commute with which other operations and thus get information that can be used by the run-time support to decide on call anticipations of operations in replicas without compromising consistency. We illustrate the formal analysis on several paradigmatic examples and briefly present a proof-of-concept implementation in Java.
翻译:分布式应用程序往往涉及具有不同一致性要求的数据:虽然在社会网络中,一个职位仅需要薄弱的一致性,但用户平衡反过来又有强烈的正确性要求,要求使突变同步。为了高效率地处理分布式应用程序不同复制件的操作顺序,有必要了解哪些业务与其他业务通勤,从而了解何时可以预期不需要同步的操作需要其他业务,从而避免不必要的等待。在这里,我们提出了一个基于语言的静态分析,以便在编译时从代码信息中提取出哪些业务可以与哪些其他业务通勤,从而获得运行时支持可以使用的信息,以便在不损及一致性的情况下决定对复制业务的呼唤预期。我们举例说明了对几个范例的正式分析,并简要介绍了在爪哇实施概念的证明。