182 research outputs found
Synchronizing the Asynchronous
No full textSynchronous programs are easy to specify because the side effects of an operation are finished by the time the invocation of the operation returns to the caller. Asynchronous programs, on the other hand, are difficult to specify because there are side effects due to pending computation scheduled as a result of the invocation of an operation. They are also difficult to verify because of the large number of possible interleavings of concurrent computation threads. We present synchronization, a new proof rule that simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Modular verification is enabled via pending asynchronous calls in atomic summaries, and a complementary proof rule that eliminates pending asynchronous calls when components and their specifications are composed. We evaluate synchronization in the context of a multi-layer refinement verification methodology on a collection of benchmark programs
Model Checking Algorithms for CTMDPs
No full textContinuous Stochastic Logic (CSL) can be interpreted over continuoustime Markov decision processes (CTMDPs) to specify quantitative properties of stochastic systems that allow some external control. Model checking CSL formulae over CTMDPs requires then the computation of optimal control strategies to prove or disprove a formula. The paper presents a conservative extension of CSL over CTMDPs—with rewards—and exploits established results for CTMDPs for model checking CSL. A new numerical approach based on uniformization is devised to compute time bounded reachability results for time dependent control strategies. Experimental evidence is given showing the efficiency of the approach
A critical analysis of the plays of Sarah Daniels.
No full textAs one of the forerunners of 'second wave' feminist playwriting, Sarah Daniels has for the
past fifteen years been one of Britain's most prolific writers for the stage. This thesis is the
first to offer a detailed critical analysis of all her published plays along with a developmental
account of her career. My approach throughout is text-based and non-prescriptive,
although I do at certain points indicate where Daniels reflects or voices differing feminist
perspectives. I also consider, beginning in Chapter Three, the critical reception and
'gendered' reviewing the playwright has received over the years.
The thesis is organised into five chapters with an Afterword. Chapter One, the
Introduction, offers an overview of Daniels' career as well as certain key characteristics of
her work. In Chapter Two I analyse the early plays, Ripen Our Darkness, The Devil's
Gateway and Neaptide, and consider in particular how they reflect, along with other
women's playwriting at the time, certain ideals of the Women's Liberation Movement.
Chapter Three is devoted entirely to Masterpieces, Daniels' most controversial and, on
many levels, successful play to date. Chapter Four is an analysis of the 'history plays',
Byrthrite and The Gut Girls. In addition to giving voice to women traditionally silenced in
and by history, these plays (especially Byrthrite) also echo particular strands of modern
feminist debate. Chapter Five examines Daniels' plays of the 1990s (Beside Herself, Head-
Rot Holiday and The Madness of Esme and Shaz) with their central theme of 'women and
madness'. This is also a fitting theme with which to conclude the thesis as it brings together
and expands on the most significant motif running throughout the playwright's work. In the
Afterword I consider the effect of Esme and Shaz's critical reception on Daniels, as well as
her current 'work in progress'. Finally, the two Appendices provide a chronological table of
Daniels' productions and a list of subsequent professional productions as well as awards
Algorithmic techniques for predictive testing of concurrent programs and distributed systems
No full textThe rise of multicore hardware platforms has lead to a new era of computing. In order to take full advantage of the power of multicore processors, developers need to write concurrent code. Unfortunately, as a result of the non-determinism introduced by thread scheduling, multi-threaded programs can show different behaviors even for a single input. Errors in concurrent programs often occur under subtle interleaving patterns that the programmer had not foreseen. There are too many interleavings to explore, even on a fixed test input for a concurrent program, making concurrency testing a hard problem.
Current testing technologies such as stress testing (running the program under test repeatedly with randomized sleep statements and by varying parameters on different platforms) have proved largely inadequate in exposing such subtle interleavings. Among the various techniques to test concurrent programs, the prediction-based technique is one of most valuable technology. Starting from one arbitrary concurrent execution of the program under testing, alternate interleavings that are likely to contain bugs are predicted. In our research, we explore prediction algorithms based on a combination of static analysis and logical constraint solving to efficiently and effectively test concurrent programs.
The strength of our research lies in the fact that the techniques we propose are general enough to predict, with a high degree of accuracy of feasibility, various kinds of concurrent errors. We provide evidence that such an approach is promising in testing concurrent programs. In fact, we have implemented our techniques in a framework, Penelope. We evaluate it over benchmark programs and find scores of null-pointer dereferences, data-races, atomicity violations and deadlocks by using only a single test run as the prediction seed for each benchmark.
We also take into account the challenge of bringing our experience in predictive testing of concurrent programs to the distributed systems environment.
We use supervised machine learning to model the system behaviors in response to perturbations, based on recorded observations in a pseudo distributed (small-scale) setting.
From the learned model, we predict the next system state given current states and applied perturbations. In a perturbation-based testing framework, accurate prediction helps to shorten the waiting time between the consecutive perturbations.
Moreover, from the learned model, we reconstruct a possible sequence of perturbation from a given sequence of observed system states for diagnosis.
We demonstrate the usefulness of our approach in a case study of a distributed system based on ZooKeeper and SolrCloud.Item withdrawn by Laura Spradlin ([email protected]) on 2014-04-25T13:33:30Z
Item was in collections:
University of Illinois Theses & Dissertations (ID: 1)
No. of bitstreams: 1
Sorrentino_Francesco.pdf: 4116711 bytes, checksum: e2abefccbd9b13b261557d91a7145ee7 (MD5)Made available in DSpace on 2014-05-30T17:06:04Z (GMT). No. of bitstreams: 2
Francesco_Sorrentino.pdf: 4116399 bytes, checksum: a07575b60585ecbcb5acee9eed0206ff (MD5)
license.txt: 4070 bytes, checksum: 9b3bb6a226d2b64324b758fadf52563e (MD5)Item marked as restricted to the 'UIUC Users [automated]' Group (id=2) by Seth Robbins ([email protected]) on 2014-05-30T17:09:48Z
Item is restricted until 2016-05-30T17:09:03ZRestriction data tranferred 2014-07-01T11:39:01-05:00
Original Data
Group with Access UIUC Users [automated]
Release Date: 2016-05-30 12:09:03 UTC
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Only Restriction Lifted for Item 49764 on 2016-09-22T20:59:12Z
On the Impact of Diagram Layout: How Are Models Actually Read?
No full textThis poster presents the latest results from a very large eye tracking study (n=29) that explores how modelers read UML diagrams. We find that various factors like layout quality, modeler experience, and diagram type lead to significant differences in diagram reading strategies. We derive elements of a theory of diagram reading behavior from our findings. This paper presents only late breaking results: all findings presented, theories constructed, and conclusions drawn are of a preliminary nature. This paper does not present the amount and degree of evidence that would allow us to consider the contents as being scientifically validated, yet
Hypersonic - Model Analysis as a Service
No full textHypersonic is a Cloud-based tool that proposes a new approach to the deployment of model analysis facilities. It is implemented as a RESTful Web service API o_ering analysis features such as model clone detection. This approach allows the migration of resource intensive analysis algorithms from monolithic desktop modeling tools to a wide range of mobile and Web-based clients. As a technology demonstrator, a Web application acting as a client for the Hypersonic API has been implemented and made publicly available
Joint Proceedings of MODELS 2014 Poster Session and the ACM Student Research Competition (SRC)
No full text
Debugging concurrent programs with sequential analysis
No full textThe design of concurrent programs is error-prone due to the interaction between concurrently executing threads. Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings. Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity. In this paper, we present a novel analysis technique for concurrent programs that avoids this exponential complexity. Our analysis transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program. The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution. Our technique never reports false errors but may miss errors. We have implemented the technique in KIS, an automated checker for multithreaded C programs, and obtained promising initial results by using KIS to detect race conditions in Windows device drivers. 1
- …
