Deductive synthesis of the unification algorithm

The deductive approach is a formal program construction method in which the derivation of a program from a given specification is regarded as a theorem-proving task. To construct a program whose output satisfies the conditions of the specification, we prove a theorem stating the existence of such an output. The proof is restricted to be sufficiently constructive so that a program computing the desired output can be extracted directly from the proof. The program we obtain is applicative and may consist of several mutually recursive procedures. The proof constitutes a demonstration of the correctness of this program.To exhibit the full power of the deductive approach, we apply it to a nontrivial example—the synthesis of a unification algorithm. Unification is the process of finding a common instance of two expressions. Algorithms to perform unification have been central to many theorem-proving systems and to some programming-language processors.The task of deriving a unification algorithm automatically is beyond the power of existing program synthesis systems. In this paper,we use the deductive approach to derive an algorithm from a simple, high-level specification of the unification task. We will identify some of the capabilities required of a theorem-proving system to perform this derivation automatically.     

基于K Framework的向量化机器学习指令语义形式化

ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术,并命名为ARM Helium,声明能为ARM Cortex-M处理器提升达15倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟程序,片上应用程序开发的依据,是程序正确性基本保障.主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究.基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码,并将其转换为形式化语义转换规则.通过K Framework提供的可执行框架利用测试用例,验证机器学习指令算数运算执行的正确性.     

Structured Theory Development for a Mechanized Logic

Experience has shown that large or multi-user interactive proof efforts can benefit significantly from structuring mechanisms, much like those available in many modern programming languages. Such a mechanism can allow some lemmas and definitions to be exported, and others not. In this paper we address two such structuring mechanisms for the ACL2 theorem prover: encapsulation and books. After presenting an introduction to ACL2, this paper justifies the implementation of ACL2s structuring mechanisms and, more generally, formulates and proves high-level correctness properties of ACL2. The issues in the present paper are relevant not only for ACL2 but also for other theorem-proving environments.     

A Mechanically Checked Proof of Correctness of the AMD K5 Floating Point Square Root Microcode

We present a rigorous mathematical proof of the correctness of the floating point square root instruction of the AMD K5 microprocessor. The instruction is represented as a program in a formal language that was designed for this purpose, based on the K5 microcode and the architecture of its FPU. We prove a statement of its correctness that corresponds directly with the IEEE Standard. We also derive an equivalent formulation, expressed in terms of rational arithmetic, which has been encoded as a formula in the ACL2 logic and mechanically verified with the ACL2 prover. Finally, we describe a microcode modification that was implemented as a result of this analysis in order to ensure the correctness of the instruction.     

Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability

We have verified the FM9801, a microprocessor design whose features include speculative execution, out-of-order issue and completion of instructions using Tomasulo's algorithm, and precise exceptions and interrupts. As a correctness criterion, we used a commutative diagram that compares the result of the pipelined execution from a flushed state to another flushed state with that of the sequential execution. Like many pipelined microprocessors, the FM9801 may not operate correctly if the executed program modifies itself. We discuss the condition under which the processor is guaranteed to operate correctly. In order to show that the correctness criterion is satisfied, we introduce an intermediate abstraction that records the history of executed instructions. Using this abstraction, we define a number of invariant properties that must hold during the operation of the FM9801. We verify these invariant properties, and then derive the proof of the commutative diagram from them. The proof has been mechanically checked by the ACL2 theorem prover.     

基于RISC-V架构的强化学习容器化方法研究

RISC-V作为近年来最热门的开源指令集架构,被广泛应用于各个特定领域的微处理器,特别是机器学习领域的模块化定制.但是,现有的RISC-V应用需要将传统软件或模型在RISC-V指令集上重新编译或优化,故如何能快速地在RISC-V体系结构上部署、运行和测试机器学习框架是一个亟待解决的技术问题.使用虚拟化技术可以解决跨平台...     

Processor allocation in a multi-ring dataflow machine

The performance of a multiprocessor architecture is determined both by the way the program is partitioned into processes and by the way these processes are allocated to different processors. In the fine-grain dataflow model, where each process consists of a single instruction, decomposition of a program into processes is achieved automatically by compilation. This paper investigates the effectiveness of fine-grain decomposition in the context of the prototype dataflow machine now in operation at the University of Manchester. The current machine is a uniprocessor, known as the Single-Ring Dataflow Machine, comprising a single processing element which contains several units connected together in a pipelined ring. A Multi-ring Dataflow Machine (MDM) containing several such processing elements connected together via an interprocessor switching network, is currently under investigation. The paper describes a method of allocating dataflow instructions to processing elements in the MDM, and examines the influence of this method on selection of a switching network. Results obtained from simulation of the MDM are presented. They show that programs are executed efficiently when their parallelism is matched to the parallelism of the machine hardware.     

对数函数ln(x)在SDTA指令集结构上的实现

SDTA指令集体系结构是一种基于传输触发的VLIW体系结构。本文结合SDTA指令集结构的特点,经过循环展开和循环化简、强度消弱、过程集成、机器方言和指令归并等指令调度优化技术,高效实现了自然对数函数ln(x)。实验结果表明,在Neuron处理器上,ln(x)不但数据精度高,而且运行周期数只有gcc3.2.2数学库中自然对数函数运行周期数的33%左右。     

Bidirectional Grammars for Machine-Code Decoding and Encoding

Binary analysis, which analyzes machine code, requires a decoder for converting bits into abstract syntax of machine instructions. Binary rewriting requires an encoder for converting instructions to bits. We propose a domain-specific language that enables the specification of both decoding and encoding in a single bidirectional grammar. With dependent types, a bigrammar enables the extraction of an executable decoder and encoder as well as a correctness proof showing their consistency. The bigrammar DSL is embedded in Coq with machine-checked proofs. We have used the bigrammar DSL to specify the decoding and encoding of subsets of the x86-32 and MIPS instruction sets. We have also extracted an executable decoder and encoder from the x86 bigrammar with competitive performance.     

Solution of the Robbins Problem

In this article we show that the three equations known as commutativity,associativity, and the Robbins equation are a basis for the variety ofBoolean algebras. The problem was posed by Herbert Robbins in the 1930s. Theproof was found automatically by EQP, a theorem-proving program forequational logic. We present the proof and the search strategies thatenabled the program to find the proof.     

Using Event-B to construct instruction set architectures

The instruction set architecture (ISA) of a computing machine is the definition of the binary instructions, registers, and memory space visible to an executable binary image. ISAs are typically implemented in hardware as microprocessors, but also in software running on a host processor, i.e. virtual machines (VMs). Despite there being many ISAs in existence, all share a set of core properties which have been tailored to their particular applications. An abstract model may capture these generic properties and be subsequently refined to a particular machine, providing a reusable template for development of robust ISAs by the formal construction of all normal and exception conditions for each instruction. This is a task to which the Event-B (Metayer et al. in Rodin deliverable 3.2 Event-B language, , 2005; Schneider in The B-method an introduction, Palgrave, Basingstoke, 2001) formal notation is well suited. This paper describes a project to use the Rodin tool-set (Abrial in Formal methods and software engineering, Springer, Berlin, 2006) to perform such a process, ultimately producing two variants of the MIDAS (Microprocessor Instruction and Data Abstraction System) ISA (Wright in Abstract state machines, B and Z, Springer, Berlin, 2007; Wright in MIDAS machine specification, Bristol University, , 2009) as VMs. The abstract model is incrementally refined to variant models capable of automatic translation to C source code, which this is compiled to create useable VMs. These are capable of running binary executables compiled from high-level languages such as C (Kernighan and Ritchie in The C programming language, Prentice-Hall, Englewood Cliffs, 1988), and compilers targeted to each variant allow demonstration programs to be executed on them.     

An integrated functional performance simulator

Microprocessor designers use multiple simulation tools with varying degrees of modeling details ranging from the instruction set of the microprocessor to the circuit implementation. We focus on tool design for the development of microarchitectures, which implement the instruction set. Microarchitecture design involves both functional and performance simulators. A functional simulator models a machine's architecture, or instruction set, with functional correctness. A performance simulator models the machine organization, or microarchitecture, and is concerned with machine performance. Sometimes these performance simulators are also referred to as cycle-accurate simulators to reflect their concern with timing issues. The FMW PowerPC-based simulation tool will help designers accurately evaluate the effectiveness and validate the correctness of new microprocessor mechanisms     

Towards dependable development tools for embedded systems: a case study in software verification

This case study describes the specification and formal verification of the key part of SPaS, a development tool for the design of open loop programmable control developed at the University of Applied Sciences in Leipzig. SPaS translates the high-level representation of an open loop programmable control into a machine executable instruction list. The produced instruction list has to exhibit the same behaviour as suggested by the high-level representation. We discuss the following features of the case study: characterization of the correctness requirements, design of a verification strategy, the correctness proof, and the relation to the Common Criteria evaluation standard.     

Formal verification of a generic framework to synthesize SAT-provers

We present in this paper an application of the ACL2 system to generate and reason about propositional satisfiability provers. For that purpose, we develop a framework in which we define a generic S AT-prover based on transformation rules, and we formalize this generic framework in the ACL2 logic, carrying out a formal proof of its termination, soundness, and completeness. This generic framework can be instantiated to obtain a number of verified and executable SAT-provers in ACL2, and this instantiation can be done in an automated way. Three instantiations of the generic framework are considered: semantic tableaux, sequent calculus, and Davis-Putnam-Logeman-Loveland methods.     

Trace specifications: methodology and models

The authors summarize the trace specification language and present the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing formal, executable models from specifications written using the methodology. These models are useful as proof of specification consistency and as executable prototypes. Fully worked examples of the methodology and the model building techniques are included     

Mothers of Pipelines

We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.     

An FPGA-based low-cost VLIW floating-point processor for CNC applications

In the high-speed free-form surface machining, the real-time motion planning and interpolation is a challenging task. This paper presents the design and implementation of a dedicated processor for the interpolation task in computerized numerical control (CNC) machine tools. The jerk-limited look-ahead motion planning and interpolation algorithm has been integrated in the interpolation processor to achieve smooth motion in the high-speed machining. The processor features a compactly designed floating-point parallel computing architecture, which employs a 3-stage pipelined reduced instruction set computer (RISC) core and a very long instruction word (VLIW) floating-point arithmetic unit. A new asynchronous execution mechanism has been employed in the processor to allow multi-cycle instructions to be performed in parallel. The proposed processor has been verified on a low-cost field programmable gate array (FPGA) chip in a prototype controller. Experimental result has demonstrated the significant improvement of the computing performance with the interpolation processor in the free-form surface machining.     

微处理器数据通路控制单元的研究与实现

在阐述精简指令集计算机数据通路基本结构的基础上,结合四种基本的指令类型及指令的执行步骤,分析了数据通路控制单元工作的基本原理,并介绍了设计与实现这种控制单元的方法,通过数字时序系统的通用方法即有限状态机的方法,将状态机的输出作为控制信号,而状态输入和指令段数据作为状态机的输入。结论证明这种设计方法能很方便地在硬件上得到实现。     

软件流水中隐式控制流恢复技术

具有条件分支的循环通过IF转换将显式的控制流转换为隐式的控制流,从而为指令调度提供进一步的机会.但它往往将程序的代码进行深度重构,增加了程序的理解和代码重建工作的复杂性.提出了一种软件流水循环中的隐式控制流恢复技术,用于重构软件流水循环中的条件分支,提高软件逆向工程中生成的目标代码的质量.