Static cecking of interrupt-driven software

Static Checking of Interrupt-driven Software

Dennis Brylow Niels Damgaard Jens Palsberg

Purdue University Department of Computer Science

Proceedings of ICSE’01, International Conference on Software Engineering, pages 47–56, 2001

Abstract

다양한 임베디드 기계들이 유비쿼터스화 되고 있다 

소프트웨어의 단순하고 명료성의 희생 없이 디바이스는 요구되는 기능을 하는것이 어렵다. 

복잡한 임베디드 시스템 때문에 개발 비용과 유지 비용이 더 많이 필요하게 된다. 이것은 특히 시스템이 assembly language로 구 성되어 있을경우 두두러진다. Static checking은 잠재적으로 이러한 문제를 완화할 수 있다.

In this paper we present the design and implementation of a static checker for interrupt-driven Z86-based software with hard real-time requirements

이들이 만든 checker는 인터럽트 지연시간 그리고 스택 크기의 상한값을 만들고 또한 기본적인 안정석과 liveness(사용여부)properties를 확인한다. 이들은 널리 알려진 model checking of pushdown systems를 바탕으로 접근했다.

그리고 control-flow graph 주석을 만들었다 with 시간, 공간, 안정성, liveness

Our tool is one of the first to give an efficient and useful static analysis of assembly code.

// 여기까지 들어도 먼말인지 잘 이해 가 되지 않음 Z86 바탕이라는것은 임베디드 마이크로 컨트롤러 시리즈를 말하는 것이다.

1 INTRODUCTION

Overview

한정된 자원을 가지는 디바이스들은 유비쿼터스화 되고 있다. 이는 소프트웨어의 단순성과 명확성을 희생하지 않고 장치에 필요한 기능에 맞게 하는것이 어려울 수 있다. 임베디드 시스템의 복잡도 향상은 extensive brute-force testing와 making development and

maintenance costly.

이들은 인터럽트를 지향하는 작은 디바이스에 집중한다. 예를 들어 Z86E30이 고려된다. Z8 processor의 자손이다. The Z86 features 256 8-bit registers,4K of instruction ROM, and 24 I/O lines organized into threeports. In addition, the Z86 has six levels of vectored interrupt processing, and two internal timers. 빈약한 자원에도 불구하고  더 큰 좋은 프로세서가 가격 경쟁력이 없는 정교한 시스템에서 사용된다. 이러한 많은 시스템들이 z86의 rem rom i/o에 한계를 가진다. operating five heating/cooling units, watching four temperature sensors, monitoring 60-cycle power for brown-outs(절전 시기), networking with a system overseer via RS–485 serial port and displaying all of its readings on an intelligent LCD unit, all in real time.// 온도 조절 시스템의 예를 들었는데 생각보다 처리 해야 할 task들이 많고 이것을 real-time으로 구현해야 한다. 

이러한 애플리케이션들은 어셈블리 언어를 통하여 컨트롤러를 볼통으로 만들기도 한다. 롬의 모든 바이트를 쥐어 짜야 하고 램의 모든 레지스터들을 사용해야 한다. 

이들은 인터럽트 지향하는 작은 프로세서를 위한 프로그래밍을 지원하는 툴에 대하여 흥미를 가지고 있다. z86과 모토로라는 작은 명령어 집합과 몇개 안되는 인터럽트를 가지고 있다 그러나 z86은 백터 인터럽트 핸들링의 강력한 능력을 유지하고 있다. 새로운 프로그래밍 도구를 만들기에 매력적인다. 

We have designed and implemented a tool that supports three tasks that usually consume a significant part of a Z86- programmer’s time

Stack-Size Analysis:

z86은 256 바이트의 스택을 레지스터공간에 가지고 있다, 이것은 스택이 오버 플로우가 발생하지 않는것은 매우 중요하다. 오엽된 데이터가 다른 프로그램에 사용이 된다면 안된다. Our tool gives upper and lower bounds on the maximum stack size.

Type Checking of Stack Elements:

스택은 pop 명령어나 인터럽트 핸들러 동작이 마무리되고 호출 프로시져로 돌아가는 둘중하나의 경우이다. 

이들은 시스템의 타입을 절대적으로 4가지로 나누었다. 

interrupt information, code address, interrupt mask, unknown.

우리의 도구는 스택의 상단에 데이터가 적절한 시간에 적절한 형식을 가지고 확인한다.

Interrupt-Latency Analysis:

We study microcontrollers that need to handle interrupts within hard realtime bounds. Our tool gives upper bounds on the latencies.

The problem

어셈블리 프로그램이 주어졌을떄, 이들은 처음으로 flow graph를 만들고 난 후 flow graph에서 원하는 분석을 실행한다. 

핵심적인 질문은 flow graph안에 노드에 Z86-machine state를 추상화 하는 방법이다. 

How much of a Z86-machine state should be represented in a flow-graph node?

하나의 근단적선택은 Z86-machine state의 모든 노드를 포함하는 것이다. 

Such a flow graph would be huge, that is, in the worst case, 2의 2048개 까지 된다. 그것은 현재 만은 노드를 표현하는 수단을 넘는다. 

또다른 근단적인선택은 오신 프로그램 카운트 PC만을 나타내는 것이다. 이러한 flow graphs는 C프로그램들 간의 interprocedural analysis하기 유용하다. 그러나 그것은 백터화된 인터럽트의 존재하에서 작은값이다 // ??

컨트롤러가 인터럽트 핸들러에 전송하게 되면 현 주소는 스택에 저장이되고 모든 인터럽트는 비활성화 된다. 만약에 인터럽트의 활성화 비활성와를 기록하는 IMR(interrupt mask register)를 모델링 라지 않는 경우 분석한 내용이 인터럽트 중첩이 발생할 수 있다고 판단할 수 있다고 생각하는데 그 이유는 컨트롤러에 신호가 도착하면 바로 핸들링이 된다고 판단하기 때문이다. 이 과정은 반복될 수 있며 결과 적으로 분석관점에서 스택에 제한업이 계속 들 성장할 수 있다고 생각 하게 된다. 

IMR을 모델링하지 않는 또 다른 결과는 흐름 그래프의 거의 모든 노드에 대해, 그것은 인터럽트가 그 시점에 도착하면, 그 인터럽트가 시간의 한정된 시간 내에 처리 할 것을 보장 할 수 없다는 것입니다. 문제의 핵심은 노드가 인터럽트 핸들러와 하나 이상의 다른 outgoing edge 있다면(2개의 outgoing edge존재한다면 ), 우리는 인터럽트가 활성화되어 있다고 가정 할 수 없다는 것입니다

we cannot conclude that the interrupt handler will be called at that point. 이 같은 모든 노드에 해당 될 것이며, 따라서 우리는 인터럽트가 처리 할 확실한 결론을 내릴 수 없다.

위와 같은 관찰을 통하여 이들은 적어도 IMR의 일부분 이라도 모델링 해야 한다는 점을 분명히 알 수 있다.

The IMR consists of seven bits, of which one is the “masterbit” which enables or disables all interrupt processing, and six others enable or disable individual interrupts.An interrupt will only be handled if both the masterbit and its “own” bit are set

When an interrupt handler is called, the masterbit is automatically turned off. 만약 인터럽트가 도착 즉시 처리 되지 않는경우 it will wait (in the IRQ register) until the IMR changes to a value that entails that the interrupt can be handled.

One could consider modeling the PC and the masterbit of the IMR.  이것도 쓸모가 없다. 인터럽트 핸들러 내부에서 가끔 마스터 비트를 제어 하는 경우가 있다. 이러한 경우가 발생하면 분석은 같은 핸들러 내부에서 발생한다고 생각하고 제한 없이 스택의 크기를 판단하게 된다. 

결론은 Our choice is to model the PC and the IMR in their entirety 이다.

일단벅으로 z86의 어셈블리 프로그램의 라인은 2의 10승 개이다 그이유는 rom의 크기가 4K이기 때문이다. 그리고 IMR는 7개의 비트로 구성되어 있다. 그렇기 때문에 노드의 상한 갯수는 2의 17개 이다. 이 방법의 그해프는 종종 C 프로그램의 분석에서 부족할수 도 있다는 있다. It may be possible to model some abstraction of the PC and the IMR; however, we did not investigate this idea.

비록 이방법이 평범하지도 명확하지도 않지만 이것은 레스터터 모델에 도움이 될것이다. 지금의 핵심 질문은 다음과 같다. 

Can modeling just the PC and the IMR lead to a useful programming tool?

In other words, can the modeling of the PC and the IMR be a good middle ground between modeling the whole machine and modeling the PC? 

Our criteria for usefulness are given by

- the degree to which the flow graph is a good basis for the three kinds of checks that we want a tool to support:

stack-size analysis, type-checking of stack elements, and interrupt-latency analysis

- the amount of time and space it takes to build the flow graph and do the checks.

본 논문의 목적은 위의 질문의 실험 평가를 제시하는 것입니다. 

our results

Z86 어셈플리 프로그래으로 부터 이들이 만든 툴은 PC와 IMR를 나타내는 각각의 노드가 있는 flow graph를 만든다. flow graph를 가지도 3가지 종류의 검사를 한다. 우리는 또한 Z86의 소프트웨어 시뮬레이터를 구축하고 최대 스택 크기에 대한 하한을 찾기 위해 그것을 사용하고 있습니다.After experiments with seven proprietary microcontrollers, our results are the following.

Stack-Size Analysis:

이들이 만든 툴은 우수한 성능을 보딘다. 정확하거나 하한값보다 최대 두개 더있는 정도의 좋은 최대 스택 크기 추정치를 계산이 가능하였다. 

Type Checking of Stack Elements:

성공

Interrupt-Latency Analysis: 

79% 까지의 produced finite latencies를 생산하였다. // 먼가 모델링으로 커버링 못한 부분있다. 

나머지 노드에 대해서 툴은 찾았다. // 나머지 21% 부분을 찾았다는 말같음 

1) there were indeed paths from those nodes to the interrupt handlers 

2) there were cycles (potentially infinite loops) in the graph that made it impossible for the analysis to guarantee finite latencies.

2 EXAMPLE

예제에 대하여 설명한다. 각각의 노드는 2가지 부분으로 나누어 진다. PC와 IMR 정보 IMR 2비트로 표현되는데 첫번째는 마스터 비트이고 두번째는 IRQ0 비트이다 이 예제에서는 IRQ0만 일어 난다. 

// 출력 논문에 정의 하였음 

Interrupt-Latency Analysis

우리는 latency(n), 그것의 핸들러가 호출 될 때까지 HPI 노드 n에 도착했을 때부터 취할 수있는 가장 긴 시간 인 노드 n에서 대기 시간을 나타 내기 위해 사용합니다.Our goal is to provide a conservative estimate of  latency(n) for all nodes n.

4 EXPERIMENTAL RESULTS

Framework and Benchmarks