Windows98下硬件中断驱动程序的开发

介绍了Ｗｉｎｈｄｏｗｓ９８的内核管理机制和应用程序权限级别,简述了在Ｗｉｎｄｏｗｓ９８下进行虚拟驱动程序开发的几种工具和编程方法,并给出一借助ＶＴｏｏｌｓＤ用Ｃ＋＋语言编写的处理硬件中断的程序实例。     

Windows98环境下数据采集的硬件中断实现

本文论证了Windows98环境下实现硬件中断的可行性并介绍了其实现的具体方法,通过在温室控制系统数据采集中的应用验证了此方法的有效性。     

一种汇编程序的形式验证框架

在高可信软件的各种性质中,安全性是关注的重点.软件满足安全策略的证明方法是安全性研究的热点之一.根据前期提出的安全程序设计与证明的框架以及指针逻辑推理系统,介绍在所实现的出具证明编译器(certifying compiler)原型系统中有关目标机器的形式定义、汇编程序的形式验证框架以及汇编程序指针程序性质证明等方面的研究.它们的主要特点是汇编验证框架是基于Hoare风格的程序验证方式;与指针有关的性质使用和源语言一级类似的指针逻辑推理系统进行证明;使用一个简单的类型系统完成有关指针的类型检查.     

用Java程序演示线程的并行执行

线程是现代计算机操作系统中的最重要概念之一,本文利用Java支持多线程编程的特性,设计出了两个演示多线程并行执行的Java程序,对于理解线程的概念能起到非常好的帮助。     

用C++Builder为接口开发设计应用程序

介绍了驱动程序的模型、可执行文件的执行原理及格式,分析了Borland公司和Microsoft公司在obj文件l、ib文件格式方面的不同,得出二者不能通用的原因,最后介绍如何用C Builder为DLL生成自己需要的lib文件。文中内容对C Builder用户、Delphi用户在接口编程开发上有一定的指导作用。     

用C++Builder为接口开发设计应用程序

介绍了驱动程序的模型、可执行文件的执行愿理及格式，分析了Borland公司和Microsoft公司在obj文件、lib文件格式方面的不同，得出二者不能通用的原因，最后介绍如何用C＋＋ Builder为DLL生成自己需要的lib文件。文中内容对C＋＋Builder用户、Delphi用户在接口编程开发上有一定的指导作用。     

Certifying assembly programs with trails

In this paper, we introduce a new way of certifying assembly programs. Unlike previous program logics, we extract the control-flow information from the code and generate an intermediate trail between the specification and the real code. Trails are auxiliary specifications and treated as modules in the certification process. We define a simple modular program logic called trail-based certified assembly programming (TCAP) to certify and link different parts of a program using the corresponding trails. Because the control flow information in trails is explicit, the rules are easier to design. We show that our logic is powerful enough to prove partial correctness of assembly programs with features including stack-based abstractions and self-modifying code.We also provide a semantics for TCAP and prove that the logic is sound with respect to the semantics.     

Preemptive scheduling with release times and deadlines

We consider the problem of deciding if there is a feasible preemptive schedule for a set of n independent tasks with release times and deadlines on m identical processors. The general problem is known to be solvable in O(n ³) time. In this paper, we study special cases for which faster algorithms exist. We introduce the notion of monotone schedules and study their properties. These properties are then exploited to devise fast algorithms for two special cases—the nested task systems and the non-overlapping task systems. We give an O(n log mn) time algorithm and an O(n log n+mn) time algorithm for nested task systems and non-overlapping task systems, respectively. Our algorithms generate at most O(n) and O(mn) preemptions for nested task systems and nonoverlapping task systems, respectively.Research supported in part by the ONR grant N00014-87-K-0833.     

Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certificate that can be used to verify that the object code satisfies desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certificate immediately after compilation. Program safety is improved because the object code and certificate alone are sufficient to establish safety: even if the object code and certificate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certificate pass the verifier.Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code generation to produce programs that are both fast and verifiably safe. To achieve this goal, we present two new languages with explicit run-time code generation constructs: Cyclone, a type safe dialect of C, and TAL/T, a type safe assembly language. We have designed and implemented a system that translates a safe C program into Cyclone, which is then compiled to TAL/T, and finally assembled into executable object code. This paper focuses on our overall approach and the front end of our system; details about TAL/T will appear in a subsequent paper.     

Construction Sequences and Certifying 3-connectivity

Tutte proved that every 3-vertex-connected graph G on more than 4 vertices has a contractible edge. Barnette and Grünbaum proved the existence of a removable edge in the same setting. We show that the sequence of contractions and the sequence of removals from G to K ₄ can be computed in O(|V|²) time by extending Barnette’s and Grünbaum’s theorem. As an application, we derive a certificate for the 3-vertex-connectivity of graphs that can be easily computed and verified.     

Integrating User-Level Threads with Processes in Scsh

Scsh, the Scheme shell, enables concurrent system programming with portable user-level threads. In scsh, threads behave like processes in many ways: each thread receives its own set of process resources; like Unix processes, new threads can inherit resources from the creating thread. The combination of scsh's interface to the POSIX API with user-level threads creates a number of design and implementation challenges: Scsh's abstractions for managing process resources raise interesting modularity issues, particularly in connection with first-class continuations. Scsh also provides an interface to the fork system call; its implementation must avoid common pitfalls that arise with a user-level thread system. This paper describes the design and implementation of the relevant abstractions and discusses the implications for programming-language and system design.     

Interrupts and the hardware-software rendezvous — microcomputer software engineering

Notations for rendezvous of communicating processes are reviewed. The use of interrupts is considered in some examples of program designs. Concepts well known in software engineering are reiterated, but they are emphasized in relation to the hardware-software interface. The concept of an interrupt service routine is shown to be at variance with the requirements of secure program design. The alternative concept of switching to another process until the required status change occurs is shown to be a suitable substitute. This requires an implicit and dynamic setting of the interrupt vector. A structured top-down approach to the design of programs which use the traditional interrupt hardware is urged. The OCCAM language has been chosen for program notation because OCCAM was designed for the representation of parallel program activity, and interrupts inherently imply some sort of parallelism.     

Certifying DFA Bounds for Recognition and Separation

Innovations in Systems and Software Engineering - The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular...     

出具证明编译器中代码优化与程序规范转换

出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.     

Preemptive and non-preemptive scheduling of optical switches with configuration delay

Utilizing optical technologies for the design of packet switches and routers offers several advantages in terms of scalability, high bandwidth, power consumption, and cost. However, the configuration delays of optical crossbars are much longer than that of the electronic counterpart, which makes the conventional slot-by-slot scheduling methods no longer the feasible solution. Therefore, some tradeoff must be found between the empty time slots and configuration overhead. This paper classifies such scheduling problems into preemptive and non-preemptive scenarios, each has its own advantages and disadvantages. Although non-preemptive scheduling is inherently not good at achieving the above-mentioned tradeoff, it is shown, however, that the proposed maximum weight matching (MWM) based greedy algorithm is guaranteed to achieve an approximation 2 for arbitrary configuration delay, and with a relatively low time complexity O(N2). For preemptive scheduling, a novel 2-approximation heuristic is presented. Each time in finding a switch configuration, the 2-approximation heuristic guarantees the covering cost of the remaining traffic matrix to have 2-approximation. Simulation results demonstrate that 2-approximation heuristic (1) performs close to the optimal scheduling, and (2) outperforms ADJUST and DOUBLE in terms of traffic transmission delay and time complexity.     

Preemptive online algorithms for scheduling with machine cost

For most scheduling problems the set of machines is fixed initially and remains unchanged. Recently Imreh and Noga proposed adding the concept of machine cost to scheduling problems and considered the so-called List Model problem. For this problem, we are given a sequence of independent jobs with positive sizes, which must be processed non-preemptively on a machine. No machines are initially provided, and when a job is revealed the algorithm has the option to purchase new machines. The objective is to minimize the sum of the makespan and cost of machines. In this paper, a modified model of List Model is presented where preemption is allowed. For this model, it is shown that better performance is possible. We present an online algorithm with a competitive ratio of while the lower bound is 4/3. For the semi-online problem with decreasing sizes, we design an optimal algorithm with a competitive ratio of 4/3, which improves the known upper bound of 3/2. The algorithm does not introduce any preemption, and hence is also an optimal semi-online algorithm for the non-preemptive semi-online problem. For the semi-online problem with known largest size, we present an optimal algorithm with a competitive ratio of 4/3.Received: 7 June 2004, Published online: 11 November 2004This research is supported by the Teaching and Research Award Program for Outstanding Young Teachers in Higher Education Institutions of MOE, China, and National Natural Science Foundation of China (10271110, 60021201).     

Prefetching with Helper Threads for Loosely Coupled Multiprocessor Systems

This paper presents a helper thread prefetching scheme that is designed to work on loosely coupled processors, such as in a standard chip multiprocessor (CMP) system or an intelligent memory system. Loosely coupled processors have an advantage in that resources such as processor and L1 cache resources are not contended by the application and helper threads, hence preserving the speed of the application. However, interprocessor communication is expensive in such a system. We present techniques to alleviate this. Our approach exploits large loop-based code regions and is based on a new synchronization mechanism between the application and helper threads. This mechanism precisely controls how far ahead the execution of the helper thread can be with respect to the application thread. We found that this is important in ensuring prefetching timeliness and avoiding cache pollution. To demonstrate that prefetching in a loosely coupled system can be done effectively, we evaluate our prefetching by simulating a standard unmodified CMP system and an intelligent memory system where a simple processor in memory executes the helper thread. Evaluating our scheme with nine memory-intensive applications with the memory processor in DRAM achieves an average speedup of 1.25. Moreover, our scheme works well in combination with a conventional processor-side sequential L1 prefetcher, resulting in an average speedup of 1.31. In a standard CMP, the scheme achieves an average speedup of 1.33. Using a real CMP system with a shared L2 cache between two cores, our helper thread prefetching plus hardware L2 prefetching achieves an average speedup of 1.15 over the hardware L2 prefetching for the subset of applications with high L2 cache misses per cycle.     

一种类型化低级语言的设计与应用

介绍了以构造一个具有更小的需信任计算基础的Java虚拟机系统为目的的研究工作，将一种类型安全的低级语言TLL应用到Java虚拟机的即时编译器中．TLL的类型系统基于多态的类型化入演算，它具有丰富的表现力且能够编码各种高级语言的抽象．基于TLL的一个虚拟机原型系统已经实现，它可以作为实现一个具有微小的需信任计算基础的Java虚拟机的起点．     

微型抢占式多任务实时内核设计

介绍引入事件驱动观念的抢占式多任务微型实时内核——MicroStar的设计与实现;提出基于事件的优先级这一新概念。