the proceedings contain 7 papers. the topics discussed include: hardening an L4 microkernel against soft errors by aspect-oriented programming and whole-program analysis;lightweight capability domains: towards decompo...
ISBN:
(纸本)9781450339421
the proceedings contain 7 papers. the topics discussed include: hardening an L4 microkernel against soft errors by aspect-oriented programming and whole-program analysis;lightweight capability domains: towards decomposing the Linux kernel;lightweight capability domains: towards decomposing the Linux kernel;ownership is theft: experiences building an embedded OS in rust;ownership is theft: experiences building an embedded OS in rust;tapir: a language for verified OS kernel probes;and making lock-free data structures verifiable with artificial transactions.
Modern services running in cloud and edge environments need to be resource-efficient to increase deployment density and reduce operating costs. Asynchronous I/O combined with asynchronous programming provides a solid ...
详细信息
the proceedings contain 8 papers. the topics discussed include: the Cogent case for property-based testing;towards correct-by-construction interrupt routing on real hardware;programmable elasticity for actor-based clo...
ISBN:
(纸本)9781450351539
the proceedings contain 8 papers. the topics discussed include: the Cogent case for property-based testing;towards correct-by-construction interrupt routing on real hardware;programmable elasticity for actor-based cloud applications;adaptable actors: just what the world needs;theseus: a state spill-free operating system;annotations in operatingsystems with custom AspectC++ attributes;towards fine-grained, automated application compartmentalization;and Sandcrust: automatic sandboxing of unsafe components in rust.
Using non-volatile memory as main memory (NVMM) can largely improve the performance of applications, but adds to the challenge of programming - it turns out to be very error-prone to write real-world NVMM programs, es...
详细信息
ISBN:
(纸本)9781450351973
Using non-volatile memory as main memory (NVMM) can largely improve the performance of applications, but adds to the challenge of programming - it turns out to be very error-prone to write real-world NVMM programs, especially with object-oriented programming. this paper presents a field study of erroneous NVMM programs written by programmers who are trained to use a general NVMM programming interface. We performed the field study in a training workshop of 30 participants. Our observations and derived best practices offer a reference for future NVMM programming techniques design. Toward that end, we propose a taxonomy of latest NVMM programming techniques and, accordingly, a set of paradigms that can reduce the risk of NVMM-specific bugs. the paradigms incorporate a minimal NVMM library interface design and a new design pattern inspired by the field study.
Over the last decade code-based test case generation techniques such as combinatorial testing or dynamic symbolic execution have seen growing research popularity. Most algorithms and tool implementations are based on ...
详细信息
ISBN:
(纸本)9783319458922;9783319458915
Over the last decade code-based test case generation techniques such as combinatorial testing or dynamic symbolic execution have seen growing research popularity. Most algorithms and tool implementations are based on finding assignments for input parameter values in order to maximise the execution branch coverage. In this paper we first present ITEC, a tool for automated test case generation in CTRL, as well as initial results of test cases executions on one of CERN's SCADA frameworks. Our tool relies on Microsoft's Pex for its code exploration. For the purpose of using this existing test generation tool, we have to translate the proprietary CTRL code into C#, one of Pex's operatinglanguages. Our main contribution lies in detailing a formal foundation for this step through source code decomposition and anonymization. We then propose a quality measure that is used to determine our confidence into the translation and the generated test cases.
Transient hardware faults in computer systems have become widespread as shrinking structures and low supply voltages reduce the amount of energy needed to trigger a fault. this paper describes the latest improvements ...
详细信息
Among all classes of parallel programming abstractions, lock-free data structures are considered one of the most scalable and efficient thanks to their fine-grained style of synchronization. However, they are also cha...
详细信息
ISBN:
(纸本)9781450339421
Among all classes of parallel programming abstractions, lock-free data structures are considered one of the most scalable and efficient thanks to their fine-grained style of synchronization. However, they are also challenging for developers and tools to verify because of the huge number of possible interleavings that result from finegrained synchronizations. this paper addresses this fundamental problem between performance and verifiability of lock-free data structure implementations. We present TXIT, a system that greatly reduces the set of possible interleavings by inserting transactions into the implementation of a lock-free data structure. We leverage hardware transactional memory support from Intel Haswell processors to enforce these artificial transactions. Evaluation on six popular lock-free data structure libraries shows that TXIT makes it easy to verify lock-free data structures while incurring acceptable runtime overhead. Further analysis shows that two inefficiencies in Haswell are the largest contributors to this overhead.
the proceedings contain 8 papers. the topics discussed include: finding resource-release omission faults in Linux;configuration coverage in the analysis of large-scale system software;preliminary design of the SAFE pl...
ISBN:
(纸本)9781450309790
the proceedings contain 8 papers. the topics discussed include: finding resource-release omission faults in Linux;configuration coverage in the analysis of large-scale system software;preliminary design of the SAFE platform;dynamic deadlock avoidance in systems code using statically inferred effects;using declarative invariants for protecting file-system integrity;assessing the scalability of garbage collectors on many cores;and URDB: a universal reversible debugger based on decomposing debugging histories.
Rational agents must be aware of their success and failure to truly assess their own progress towards their intended goals. In this study we describe a detailed investigation of how current BDI agents monitor their su...
详细信息
ISBN:
(纸本)9783642033377
Rational agents must be aware of their success and failure to truly assess their own progress towards their intended goals. In this study we describe a detailed investigation of how current BDI agents monitor their successes and failures during their reasoning cycle. Our analysis indicates that the existing architectures are inadequate to specifically detect failures in their own behaviors. this makes them unaware of the reality of the environment in which they are operating. We propose an extended BDI-like architecture to address these problems. We extend the current reasoning cycle by reformulating the execution of actions and plans, and introducing additional rules to detect failures. the resulting reformulation can be applied to existing systems such as JACK, JAM, etc. As a case study we extended JASON to implement the extended BDI architecture.
暂无评论