Distributed software is common in the real-world but remains error-prone.  Even when the underlying logic is inherently sequential and simple, addressing distributed aspects results in complex cross-cutting code that undermines such simplicity.  The project developed methods and tools to make distributed programming more robust. One approach was to provide a clean separation of concerns and retains the simplicity of sequential computation, using it as a basis onto which distributed aspects are added without corrupting the essential sequential structure, while offloading much of the complexity of implementing distributed concerns to the compiler. The approach was demonstrated on web applications. 

New methods for ensuring the correctness of distributed programs developed include methods for specifying and inferring the concurrency structure of distributed programs, as well as for testing programs.   One area explored was to find erroneous assumptions in Java code by checking client code against models of library methods, which encode all behaviors allowed by the specifications. This was developed into a tool and demonstrated by applying to 46 tests.  The results provide new insights into the complexity of exploring the behaviors of code that uses underdetermined APIs and the structure of state spaces that arise in the exploration.  It also provides a basis for future work on better detecting faults in tests that invoke underdetermined APIs as well as developing tool support for writing and maintaining more robust test suites.   The project further developed an approach to make regression testing—the process of testing programs that continuously updated—more efficient. 

A key problem in testing distributed programs is that there are too many potential schedules (orders in which concurrent activity may take places).  The project developed methods which are effective in inferring if there are feasible schedules that could lead to problematic executions.  A tool was developed for a popular programming framework (actors) used for distributed programming in industry (AKKA).  Our evaluation showed that the tool achieved a relatively high target coverage (78% on 1,000 potentially problematic executions or targets) and detected previously unreported bugs.

The project developed a dynamic inference tool to determine the intended concurrency structure of a distributed program.  Such a structure can be expressed as pluggable types, checked and extended statically (without execution), and used as basis of transforming concurrent programs so that they are suitable for distributed execution (e.g. on the cloud and on mobile devices).  The project also developed methods for inferring the evolution of the interface of a large class of programs, as different actors change state and are unable to perform certain functions at different times.  Such evolution affects their interaction with other actors.  By ensuring that only certain invocations are made in a particular order, we can enforce interaction protocols which avoid potentially problematic behaviors.   Session type systems enable inference and enforcement of message exchange patterns for distributed programs. Essentially, session types can capture the evolution of interfaces of different actors in a system, including cross-program causal message passing dependencies.  The project developed methods for specifying and inferring mutiparty session types, both to ensure safety and, for an important class of programs, to guarantee that the system makes progress.

Many safety critical applications in the real-world, such as IoT devices, medical devices, industrial process controllers, and sensor networks, involve distributed systems.  The results of project will further research in the field and suggests a number of ways to improve the safety and reliability of such distributed software in the future.  

Last Modified: 11/26/2018
Modified by: Gul A Agha