Miscellaneous Distributed Systems

Other contributions in the general area of distributed systems include:

• Characterization of message ordering specifications: We provide necessary and sufficient condition for a message ordering specification to be implementable in a distributed system. When a message ordering specification is implementable, we provide conditions by which it can be determined whether there exists a protocol which does not use control messages but only tags extra information with application messages. (IEEE ICDCS 97).
• Verification of Distributed Programs: Introduced a technique of induction for the causally precedes relation and its complement for formal verification of distributed programs. Based on this technique provided the formal proof of correctness of vector clock algorithms. Acta Informatica 97
• Consistency Conditions The traditional Distributed Shared Memory (DSM) model provides atomicity at levels of read and write on single objects. Therefore, multi-object operations such as double compare and swap, and atomic m-register assignment cannot be efficiently expressed in this model. We extend the traditional DSM model to allow operations to span multiple objects. We show that memory consistency conditions such as sequential consistency and linearizability can be extended to this general model. We also provide algorithms to implement these consistency conditions in a distributed system. We also propose a new memory consistency condition called Normality that is equivalent to linearizability for single object operations but weaker than linearizability for multi-object operations. Normality is better suited for distributed systems because it does not refer to global-time. Normality also satisfies locality and non-blocking. (ICDCS 98, PPL 99)
• Distributed Simulation: Developed a new k-optmistic distributed simulation algorithm. This algorithm does not use anti-messages and thus not only reduces the overhead of anti-messages but also eliminates the need for output queues. In addition, the algorithm allows a seamless integration of pessimistic and optimistic simulation in one framework. This is especially useful in mixed simulation scenarios where some processes may not have ability to rollback. Also developed an efficient algorithm for bounding global virtual time which is useful for interactive simulation. (ACM PADS 93, PADS 97, PADS 98).
• Global Functions Many tasks in distributed systems consists of repeatedly computing a global function. Imposing a tree-like structure is natural to gather the arguments of the function and broadcast the result. Can we get symmetry in spite of the hierarchy. We show such a technique. The technique is illustrated for distributed branch-and-bound problem, and for asynchronous computation of fixed points. (ICDCS' 90, IEEE Trans. on Parallel & Distributed Systems 1994).
• Algebraic Characterization of Petri Net Languages: We have developed an algebraic system called concurrent regular expressions which provide a modular description of languages of Petri nets. This alternative characterization of Petri net languages gives a flexible way of specifying concurrent systems. The proof of equivalence also provides a natural decomposition method for Petri nets. Theoretical Computer Science 92.