Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCompositional Reasoning for Explicit Resource Management in Channel-Based Concurrency
193
0
0.0
(
0
)
Added by
Adrian Francalanza
Publication date
2014
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct coinductive proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. We establish full abstraction results between our coinductive definitions and a contextual behavioural preorder describing a notion of process efficiency w.r.t. its management of resources. We also justify these definitions and respective proof techniques through numerous examples and a case study comparing two concurrent implementations of an extensible buffer.
rate research
Read More
We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.
Model checking probabilistic CTL properties of Markov decision processes with convex uncertainties has been recently investigated by Puggelli et al. Such model checking algorithms typically suffer from the state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDP while preserving the probabilistic CTL properties it satisfies. In particular, we discuss the key ingredients to build up the operations of parallel composition for composing interval MDP components at run-time. More precisely, we investigate how the parallel composition operator for interval MDPs can be defined so as to arrive at a congruence closure. As a result, we show that probabilistic bisimulation for interval MDPs is congruence with respect to two facets of parallelism, namely synchronous product and interleaving.
The paper presents our research on quantifier elimination (QE) for compositional reasoning and verification. For compositional reasoning, QE provides the foundation of our approach, serving as the calculus for composition to derive the strongest system-property in a single step, from the given component atomic-properties and their interconnection relation. We first developed this framework for time-independent properties, and later extended it to time-dependent property composition. The extension requires, in addition, shifting the given properties along time to span the time horizon of interest, he least of which for the strongest system-property is no more than the total time horizons of the component level atomic-properties. The system-initial-condition is also composed from atomic-initial-conditions of the components the same way. It is used to verify a desired system-level property, alongside the derived strongest system-property, by way of induction. Our composition approach is uniform regardless of the composition types (cascade/parallel/feedback) for both time-dependent and time-independent properties. We developed a new prototype verifier named ReLIC (Reduced Logic Inference for Composition) that implements our above approaches. We demonstrated it through several illustrative and practical examples. Further, we advanced the $k$-induction based model-checking with QE capabilities, by formulating its base and inductive steps into QE problems where all the variables are universally quantified. Our integration of the QE solver Redlog with the $k$-induction based model-checking tool JKind, shows the successful solving of a non-linear problem that the SMT capable JKind failed to resolve. Finally, we also showcase the recent adoption of our approaches within an industrial V&V tool suite for augmented static analysis of Simulink models and Deep Neural Networks (DNNs).
We develop local reasoning techniques for message passing concurrent programs based on ideas from separation logics and resource usage analysis. We extend processes with permission- resources and define a reduction semantics for this extended language. This provides a foundation for interpreting separation formulas for message-passing concurrency. We also define a sound proof system permitting us to infer satisfaction compositionally using local, separation-based reasoning.
We introduce a controlled concurrency framework, derived from the Owicki-Gries method, for describing a hardware interface in detail sufficient to support the modelling and verification of small, embedded operating systems (OSs) whose run-time responsiveness is paramount. Such real-time systems run with interrupts mostly enabled, including during scheduling. That differs from many other successfully modelled and verified OSs that typically reduce the complexity of concurrency by running on uniprocessor platforms and by switching interrupts off as much as possible. Our framework builds on the traditional Owicki-Gries method, for its fine-grained concurrency is needed for high-performance system code. We adapt it to support explicit concurrency control, by providing a simple, faithful representation of the hardware interface that allows software to control the degree of interleaving between user code, OS code, interrupt handlers and a scheduler that controls context switching. We then apply this framework to model the interleaving behavior of the eChronos OS, a preemptible real-time OS for embedded micro-controllers. We discuss the accuracy and usability of our approach when instantiated to model the eChronos OS. Both our framework and the eChronos model are formalised in the Isabelle/HOL theorem prover, taking advantage of the high level of automation in modern reasoning tools.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
