Mobile processes with local clocks

We propose a structural operational semantics that expresses temporal aspects of mobile and distributed systems, each sequential component of which has its local clock. Since the run-time support of a programming language implements the operations of the language via some lower-level routines, the same action, put in different contexts, may have different durations. Also the network topology affects these durations, typically when messages are exchanged. We model this through a transition system labelled by actions and their costs, in a discrete time. Then, we define two performance preordings that say when the execution of a process is faster than that of another. The first preorder is similar to those presented in the literature, while the second refines it in that it considers a process faster than another if it is such from some point onwards of its execution. Finally, as an example we compare the performance of a conventional uniprocessor architecture with a prefetch pipeline architecture.