We introduce Pancake, a new language for verifiable, low-level systemsprogramming, especially device drivers. Pancake eschews complex type systems to make the language attractive to systems programmers, while at the ...
ISBN:
(纸本)9798400704048
We introduce Pancake, a new language for verifiable, low-level systemsprogramming, especially device drivers. Pancake eschews complex type systems to make the language attractive to systems programmers, while at the same time aiming to ease the formal verification of code. We describe the design of the language and its verified compiler, and examine its usability, performance and current limitations through case studies of device drivers and related systems components for an seL4-based operating system.
Graceful degradation is an established concept to improve the resilience of systems, especially when other resilience mechanisms have failed. Its implementation is often heavily tied to the application code and, thus,...
详细信息
Aspect Oriented programming (AOP) supports the modular implementation of crosscutting concerns, which are woven into program parts designated by pointcuts, e.g. calls to specific functions. the release of AspectC++ 2....
详细信息
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.
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 ...
详细信息
the proceedings contain 10 papers. the topics discussed include: formalising device driver interfaces;writing systems software in a functional language;towards easing the diagnosis of bugs in OS code;configurable memo...
ISBN:
(纸本)9781595939227
the proceedings contain 10 papers. the topics discussed include: formalising device driver interfaces;writing systems software in a functional language;towards easing the diagnosis of bugs in OS code;configurable memory protection by aspects;a DSL approach for object memory management of small devices;resource management aspects for sensor network software;why the grass may not be greener on the other side: a comparison of locking vs. transactional memory;predictive thread-to-core assignment on a heterogeneous multi-core processor;a high-performance operating system for structured concurrent programs;and checking the hardware-software interface in Spec#.
this manuscript presents the results achieved after using the Central Force Optimization (CFO) algorithm, proposed by Formato on 2007, for solving a system of nonlinear equations, which represents an electronic circui...
详细信息
this manuscript presents the results achieved after using the Central Force Optimization (CFO) algorithm, proposed by Formato on 2007, for solving a system of nonlinear equations, which represents an electronic circuit operating on dc. At first, a brief theoretical foundation of CFO is shown, as well as a theorem that shows why it is possible to solve this type of systemsthrough an optimization algorithm. Afterwards, its behavior for some standard functions, is commented. Moreover, results with a basic circuit, and a scalable one, are discussed. It was found that CFO does not operate well for nearly plain regions, such as the one between zero volts and the conduction voltage of a diode. this is later demonstrated by using an objective function built with a system of exponential equations. Even after a couple of modifications, CFO was not able to find a valid answer for systems of three or more variables, so it is concluded that this approach should be avoided, at least for the time being, for the solution of equations with a planar or almost planar region and the previously mentioned number of unknowns.
Managed Runtime Environments (MRE) are increasingly used for application servers that use large multi-core hardware. We find that the garbage collector is critical for overall performance in this setting. We explore t...
详细信息
Withthe advent of multi-processor machines, the time has definitively come to use new programming models that offer an improved support of concurrency. While various interesting new models have been recently presente...
详细信息
ISBN:
(纸本)9781595939227
Withthe advent of multi-processor machines, the time has definitively come to use new programming models that offer an improved support of concurrency. While various interesting new models have been recently presented for concurrent and structured programming, no appropriate runtime systems currently exists. therefore, we have developed our own new operating system which has been particularly optimized for high-performance execution of such programs. Copyright 2007 ACM concurrency, memory management, hierarchical composition, message communication.
暂无评论