My latest research focused on developing practical model checking, verification, and debug-at-scale techniques for distributed systems.
The DS2 project emerged after exploring (source code reading) an extension of IBM’s X10 project by Rice University called Habanero Java. DS2 is aimed at model checking/auto-testing of Distributed systems written in Akka-Scala (actor-based event-driven and fault tolerant parallelism). We developed a linearizability checking tool of basic distributed stores on top of it, e.g. key-value stores, that underlie most modern distributed databases, and cloud storage systems. The project resulted in two novel Dynamic Partial Order Reduction algorithms.
PhD: Project Repository.
PhD: Dissertation -- Will be posted as soon as the university provides a link.
Fast prototyping of massively parallel applications using multiple frameworks to increase programmer productivity.
Here is a link to my research report.
Latest publication first.
Efficient Linearizability Checking for Actor-based Systems, Mohammed S. Al-Mahfoudh, Ryan Stutsman, Ganesh Gopalakrishnan.
Operational Semantics for the Rigorous Analysis of Distributed Systems [Invited/extended paper], Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman
Toward Bringing Distributed Systems Design upon Rigorous Footing, Mohammed S. Al-Mahfoudh , Ganesh Gopalakrishnan, Ryan Stutsman
Toward rigorous design of domain-specific distributed systems,