SIGNAL模型多线程代码生成研究

反应式系统是指与环境不断发生交互的控制系统。这类系统通过接收外部环境输入,对输入进行计算,并将计算结果反馈到外部环境来控制系统的行为。同步语言是一种规约反应式系统的建模语言,同步语言的优势在于支持形式化验证和精确的代码自动生成。面向多时钟同步语言SIGNAL,提出了一种SIGNAL模型到多线程Java代码生成过程。该代码生成过程基于以下3种中间结构:同步时钟卫式操作、卫式操作和带划分的卫式操作。将整个代码生成过程分为4个主要转化步骤,给出每一步转化规则。最后对空客A340的警报系统进行实例分析,评估生成代码的正确性。多线程Java代码生成可以为SIGNAL模型在分布式和多核体系下的应用提供支撑。     

面向同步规范的并行代码自动生成

随着对安全攸关实时系统功能与非功能要求的日益增加,使用多核技术将成为发展趋势.如何在多核平台条件下保证系统运行的可信任性及可靠性是学术上和应用上的关键问题.目前基于形式化方法的系统设计、验证以及自动代码生成已经在单核平台上形成很多研究成果,但在多核平台上的研究仍面临许多科学问题.同步语言SIGNAL是一种被广泛应用于安全攸关实时系统功能设计的形式化方法,适用于对系统确定性并发行为的描述.SIGNAL编译器也支持将同步规范SynchronousSpecification）生成仿真代码,以对其进行验证与分析.然而现有研究较少关注从SIGNAL同步规范到支持跨平台并行代码的生成方法.本文研究面向SIGNAL同步规范的并行自动代码生成方法.提出了方程依赖图EDG的概念,将SIGNAL规范转换为EDG以分析其全局数据依赖关系;研究了对EDG进行任务划分获取规范中可以并行执行部分的算法;最后,以跨平台并行编程API-OpenMP作为对象,结合程序中信号的时钟关系,将并行任务映射到OpenMP并行代码,并进行了实例验证.     

同步语言的时间可预测多线程代码生成方法

能够提供更强计算能力的多核处理器将在安全关键系统中得到广泛应用.但是,由于现代处理器所使用的流水线、乱序执行、动态分支预测、Cache等性能提高机制以及多核之间的资源共享,使得系统的最坏执行时间分析变得非常困难.为此,国际学术界提出时间可预测系统设计的思想,以降低系统的最坏执行时间分析难度.已有研究主要关注硬件层次及其编译方法的调整和优化,而较少关注软件层次,即时间可预测多线程代码的构造方法以及到多核硬件平台的映射.本文提出一种基于同步语言模型驱动的时间可预测多线程代码生成方法,并对代码生成器的语义保持进行证明;提出一种基于AADL(Architecture Analysis and Design Language)的时间可预测多核体系结构模型,作为本文研究的目标平台;最后,给出多线程代码到多核体系结构模型的映射方法,并给出系统性质的分析框架.     

同步数据流语言可信编译器的构造

同步数据流语言近年来在航空、高铁、核电等安全关键领域得到广泛应用.然而,此类语言相关开发工具本身的安全性业已成为被高度关注的安全隐患之一.借助辅助定理证明器实现常规语言编译器的构造和验证已被证明是成功的,有望最大限度地解决误编译问题.基于这种方法,开展了从同步数据流语言(Lustre为原型)到串行命令式语言(C为原型)的可信编译器构造的关键技术研究.其挑战性在于两类语言之间的巨大差异,源语言具有时钟同步、数据流、并发及流数据对象等特征,而目标语言则具有顺序控制流特征.同类研究中,目前尚无针对核心翻译过程的公开成果.就单一时钟的情形实现了一个经过形式化验证的完整编译过程,相关技术将应用于安全关键领域编译系统的开发.综述了这一可信编译器的研究背景、意义、总体设计框架、核心技术、现状以及进行中或后续的工作.     

数据流程序动态调度与优化

为了解决数据流编程模型的可用性问题,使其能在兼顾程序并行性的前提下适用于动态数据交互速率的流应用,设计了一种动态调度与静态优化相结合的数据流编译系统。编译器以COStream语言编写的源程序为输入,通过对源程序进行分析,以动态速率的数据通信边作为边界划分程序到粗粒度的子图,在子图内部应用静态优化。根据子图的每个计算单元的工作量估计计算资源的使用状况,实现子图内计算单元到处理器核的映射,经过阶段划分分配子图内计算单元到相应流水阶段。在运行时,每个子图在各个处理器核上均启动一个线程,通过对线程间通信的优化,避免了运行时多个线程对同一段内存同时读写产生的同步开销,减少了线程的上下文切换次数。使用信号量控制子图内线程间的同步,基于各子图计算单元运行时数据交互速率并结合当前线程的状态,动态调度各个子图的执行,构建动态的软件流水线,生成相应多线程目标代码。实验以通用X86-64多核处理器作为实验平台,测试和分析数据流编译的性能。实验结果表明,编译系统可以实现动态数据交互速率的数据流应用,扩大了编译系统可用性并且具有一定加速效果。     

基于FFMPEG解码的音视频同步实现

为实现音视频同步播放,针对音视频数据同时被采集,但编码和存储独立的情况,提出了将音频播放时钟作为同步时钟,采用时间戳技术实现历史音视频同步播放.该方法使用FFMPEG对历史音视频文件分别进行解码,将解码后计算得到的音频播放时钟作为同步时钟,控制视频播放速度同步到音频播放时钟上,保证了音视频数据流畅播放,同步无滞后,无延迟.通过实验设计,验证了提出的基于音频播放时钟的时间戳同步方法是有效的.     

基于神威·太湖之光的非结构网格计算加速算法

在国产异构众核平台神威·太湖之光上的非结构网格计算具有稀疏存储、离散访存、数据依赖等特点,严重制约了众核处理器的性能发挥。为解决稀疏存储和离散访存问题,提出一种N阶对角染色算法,以有效平衡主从核计算并利用从核将全局访存转化为LDM访问。针对数据依赖造成的计算竞争问题,采用自适应和无依赖的任务划分方法,避免并行计算时的数据冲突。为对处理器架构和非结构网格计算进行优化,采用主核与从核异步并行的方式,差异化使用主从核以充分利用硬件资源,同时,取消处理器提供的寄存器通信机制,降低从核阵列的同步开销同时便于扩展到新一代神威平台。此外,使用计算访存异步重叠技术来充分隐藏访存延迟。利用SpMV、Integration、calcLudsFcc算子进行实验,结果表明,相比主核实现,组合加速算法在不同算例规模下平均取得了10倍的加速效果,加速比最高可达24倍,N阶对角染色算法相比非染色分块算法取得了超过5.8倍的性能加速,有效提升了数据局部性和计算并行度。该算法对有依赖关系的计算冲突算子同样具有良好的加速性能,验证了自适应和无依赖任务划分方法的有效性。     

一种挖掘多核处理器存储级并行的算法

多核处理器中,各个处理器核之间可以并发地进行外部存储访问,提供不同于单处理器的存储级并行(memory level parallelism)能力.不规则应用中的循环,传统的并行方法难以识别其并行性,不能充分利用多核处理器存储级并行能力和并行计算能力.对基于软件开发多核处理器存储级并行进行了讨论,提出一种前瞻并行多线程算法LLSM(loop level speculative mssultithreading).LLSM对不规则应用中的循环进行并行化,在多核处理器上的测试数据表明:该算法能够有效地挖掘多核处理器的存储级并行能力和计算能力,同时指出多核环境下存储级并行计算公式需要考虑线程同步开销.     

多核处理器中基于Radix-Join的嵌套循环连接优化

针对目前主流的多核处理器,研究了基于共享Cache多核处理器的数据库Nested Loop Join(NINLJ)优化.针对无索引情况下的NLJ,提出了基于Radix-NL-Join算法的NLJ多线程执行框架.从减少Cache访问冲突和提高Cache命中率两个方面优化了NINLJ多线程执行框架中的聚集划分和聚集连接线程.主要贡献如下:1.针对多线程访问共享Cache容易出现共享Cache访问冲突的问题,优化了聚集划分阶段的多线程聚集划分线程的启动时机;2.针对聚集连接阶段,聚集连接线程Cache访问性能不佳,利用聚集连接线程顺序访问聚集的优势,采用预取线程提高聚集连接线程的性能;3.在实验中,基于开源数据库EaseDB实现了上述多线程执行框架,测试了多线程NLJ的性能.实验结果表明,提出的NLJ多线程执行框架,可以充分利用多核处理器的计算资源,并有效地解决共享Cache在多线程条件下的Cache访问冲突问题,大大提高了NLJ的性能,相对于未采用Cache优化的多线程Radix-NL-Join算法,其性能提升了26%左右.     

基于NiosⅡ软核的工业以太网精确时钟同步的实现

介绍了基于NiosⅡ嵌入式软核处理器的工业以太网设备间精确时钟同步的设计与实现.利用Altera公司的Nios Ⅱ处理器,添加片内外设和存储器以及与片外存储器和外设相连的接口,通过SOPC(可编程片上系统)技术嵌入到FPGA芯片中形成Nios Ⅱ处理器系统硬件平台;软件部分移植uC/OS-Ⅱ作为操作系统,Lwip(轻量级TCP/IP协议)处理网络协议,在应用层上实现状态转换、同步报文处理和精确时钟算法.测试结果表明时钟同步精度高,并且最终在一个工业以太网实验平台上进行了长期的实际运行,系统稳定性良好.     

Towards a verified compiler prototype for the synchronous language SIGNAL

SIGNAL belongs to the synchronous languages family which are widely used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. This paper reports a compiler prototype for SIGNAL. Compared with the existing SIGNAL compiler, we propose a new intermediate representation (named S-CGA, a variant of clocked guarded actions), to integrate more synchronous programs into our compiler prototype in the future. The front-end of the compiler, i.e., the translation from SIGNAL to S-CGA, is presented. As well, the proof of semantics preservation is mechanized in the theorem prover Coq. Moreover, we present the back-end of the compiler, including sequential code generation and multithreaded code generation with time-predictable properties. With the rising importance of multi-core processors in safetycritical embedded systems or cyber-physical systems (CPS), there is a growing need for model-driven generation of multithreaded code and thus mapping on multi-core. We propose a time-predictable multi-core architecture model in architecture analysis and design language (AADL), and map the multi-threaded code to this model.     

Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.     

三次插值样条曲线拟合多核并行算法

充分利用多核技术提升多核处理器的资源利用率,缩短执行时间,发挥多核系统的优异性能。在多核计算机上设计了解三对角方程组的奇偶约化多线程并行程序,实现了三次样条曲线拟合的快速计算。通过实验结果的加速比对比,可以看出并行后缩短了求解方程组的时间,多核资源得到充分利用。结果表明,奇偶约化多核并行算法在三次样条曲线拟合中的应用是有效及可行的。     

消息传递并行程序的自动生成

针对分布内存结构的并行化将串行程序转变为在各处理节点上运行的SPMD并行程序,节点程序包含该节点所执行的运算和与其它节点交换信息的通信操作。讨论了在已知数据分解和计算划分的前提下生成分布内存结构下的消息传递并行程序的算法,以Lam提出的线性不等式基本框架为基础,在Paraguin工作基础上进行了有效的改进：第一在代码生成算法中引入了数据分布;第二将处理器空间由一维扩展到多维;第三将虚拟处理器到物理处理器的映射关系引入代码生成算法,从而减少了节点间通信的数量,提高了生成并行代码的性能。     

Using design space exploration for finding schedules with guaranteed reaction times of synchronous programs on multi-core architecture

The synchronous model of computation is well suited for real-time systems, because it allows static analysis in order to find and guarantee their reaction times. Today’s multi-core systems are becoming the predominant computing platforms. Synchronous programs are typically compiled into single threaded code, which makes them unsuitable for exploiting parallelism of the multi-core platforms. Moreover, static timing analysis becomes highly intractable for multi-core systems. This article proposes a novel methodology that aims at finding the mapping and schedule of synchronous programs that guarantees, statically, reaction times when mapped onto a multi-core system consisting of two types of time-predictable cores. The proposed methodology combines design space exploration based on evolutionary algorithm and scheduling of parts of synchronous programs. It allows minimizing the resource usage in terms of number of cores by finding the mapping and schedule with the guaranteed reaction time for architectures with different number of cores. In particular, we: (a) transform a synchronous program written in synchronous SystemJ to a graph-based model represented with two types of computation nodes suitable for execution on two types of time-predictable cores, (b) perform mapping of computation nodes on a customizable multi-core platform using genetic operations, and (c) generate a resulting static schedule of computation nodes for each mapping as part of the design space exploration. The design flow, from program specification and node mapping to the design space exploration and multi-core scheduling is completely automated.     

一种改进数据流图的子字并行程序表示方法

论文致力于对图像处理算法的串行C程序进行子字并行分析,并重定向到带有多媒体扩展的通用处理器和多媒体专用嵌入式微处理器。图像处理算法的特点决定其是内在可并行的,这种并行粒度介于数据并行(DLP)和指令级并行(ILP)之间,称之为子字并行。但是,当前的编译技术很难充分挖掘和定位程序基本块内的子字并行,对此设计了一种基于流图程序表示的编译方法,能够从串行程序中显式地定位子字并行。扩展了编译器的功能,增加了特定的模式库,基于模式识别的控制流和数据流分析后,产生特定的子字并行流图(SWFG,Sub-WordFlowGraph),并将该图作为中间表示,提供给子字并行指令选择,进而实现有效的子字并行代码产生。