  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.
