Tag: ebnenasir

Ali Ebnenasir is Co-Author of Publication in ACM Transactions on Computational Logic

Ali Ebnenasir
Ali Ebnenasir

An article co-authored by Ali Ebnenasir (SAS/CS) and Alex Klinkhamer, “Verification of Livelock-Freedom and Self-Stabilization on Parameterized Rings,” was recently published in ACM Transactions on Computational Logic.

Abstract: This article investigates the verification of livelock-freedom and self-stabilization on parameterized rings consisting of symmetric, constant space, deterministic, and self-disabling processes. The results of this article have a significant impact on several fields, including scalable distributed systems, resilient and self-* systems, and verification of parameterized systems. First, we identify necessary and sufficient local conditions for the existence of global livelocks in parameterized unidirectional rings with unbounded (but finite) number of processes under the interleaving semantics. Using a reduction from the periodic domino problem, we show that, in general, verifying livelock-freedom of parameterized unidirectional rings is undecidable (specifically, Π10-complete) even for constant space, deterministic, and self-disabling processes. This result implies that verifying self-stabilization for parameterized rings of self-disabling processes is also undecidable. We also show that verifying livelock-freedom and self-stabilization remain undecidable under (1) synchronous execution semantics, (2) the FIFO consistency model, and (3) any scheduling policy. We then present a new scope-based method for detecting and constructing livelocks in parameterized rings. The proposed semi-algorithm behind our scope-based verification is based on a novel paradigm for the detection of livelocks that totally circumvents state space exploration. Our experimental results on an implementation of the proposed semi-algorithm are very promising as we have found livelocks in parameterized rings in a few microseconds on a regular laptop. The results of this article have significant implications for scalable distributed systems with cyclic topologies.


doi: 10.1145/3326456

Self-Stabilizing Systems

It was August 15, 2003. A software bug invoked a blackout spanning the Northeast, Midwest, and parts of Canada. Subways shut down. Hospital patients suffered in stifling heat. And police evacuated people trapped in elevators.

What should have been a manageable, local blackout cascaded into widespread distress on the electric grid. A lack of alarm left operators unaware of the need to re-distribute power after overloaded transmission lines hit unpruned foliage, which triggered a race condition in the control software.*


Ali Ebnenasir is working to prevent another Northeast Blackout. He’s creating and testing new design methods for more dependable software in the presence of unanticipated environmental and internal faults. “What software does or doesn’t do is critical,” Ebnenasir explains. “Think about medical devices controlled by software. Patient lives are at stake when there’s a software malfunction.”

How do you make distributed software more dependable? In the case of a single machine—like a smartphone—it’s easy. Just hit reset. But for a network, there is no centralized reset. “Our challenge is to design distributed software systems that automatically recover from unanticipated events,” Ebnenasir says.

The problem—and some solutions—has been around for nearly 40 years, but no uniform theory for designing self-stabilizing systems exists. “Now we’re equipping software engineers with tools and methods to design systems that autonomously recover.”

Ebnenasir’s work has been funded by the National Science Foundation.

*Source: Wikipedia

Ali Ebnenasir receives nomination of University’s 2016 Distinguished Teaching Award!

Ali Ebnenasir
Ali Ebnenasir

Congratulations Ali on receiving the nomination of University’s 2016 Distinguished Teaching Award! According to the University’s Center for Teaching and Learning, Ali has been chosen as one of the five finalists from among all Michigan Tech teaching faculty. Selection as a finalist automatically enrolls Ali as a member of the Michigan Tech Academy of Teaching Excellence. Congratulations Ali! Thank you for your dedication to our students and your outstanding teaching performance.

Support Ali’s nomination with your comments!

Using “Superior” Supercomputer for Advanced Research

Michigan Tech is home to a supercomputer known as “Superior” and this computer is used for a variety of projects by research faculty right here in the Department of Computer Science:

Laura Brown, Towards a reliable method for comparing large scale machine learning algorithms

Ali Ebnenasir, Computational synthesis of self-stabilizing protocols

Chaoli Wang, High-performance parallel analysis and visualization of Big Data

Read more at insideHPC.