Tools and Benchmarks for Real-Time Systems

Verification challenge • Re: Calculating Latencies in an Engine Management System Using Response Time Analysis with MAST

2016-07-12T15:47:50+01:00

Here you can find the slides of our presentation:

presentation.pdf

Statistics: Posted by rivasjm — Tue Jul 12, 2016

Verification challenge • Presentation of the FMTV 2016 Challenge

2016-07-11T11:50:56+01:00

The complex dynamic behaviour of automotive software systems, in particular engine management, in combination with emerging multi-core execution platforms, significantly increased the problem space for timing analysis methods. As a result, the risk of divergence between academic research and industrial practice is currently increasing.

Therefore, we from Bosch provided a concrete automotive benchmark for the Formal Methods for Timing Verification (FMTV) challenge 2016, a full blown performance model of a modern engine management system (downloadable http://www.ecrts.org/forum/viewtopic.php?f=27&t=62), with the goal to challenge existing timing analysis approaches with respect to their expressiveness and precision.

The focus of the challenge lies on determining tight end-to-end latency bounds for a set of given cause-effect chains. This is challenging since the dynamic behavior of a engine management software is quite complex and contains mechanisms that explore the limits of existing academic approaches:

preemptive and cooperative priority based scheduling
periodic, sporadic, and engine synchronous tasks
multi-core platform with distributed cause-effect chains including cross-core communication
label (i.e. data) placement dependent execution times of runnables

FMTV2016_Presentation_Waters_2016.pdf

Statistics: Posted by arne.hamann — Mon Jul 11, 2016

Verification challenge • Schedulability and Timing Analysis of Mixed Preemptive-Cooperative Tasks on a Partitioned Multi-Core System

2016-07-01T17:02:46+01:00

Title: Schedulability and Timing Analysis of Mixed Preemptive-Cooperative Tasks on a Partitioned Multi-Core System

Authors:
Ignacio Sañudo, Paolo Burgio and Marko Bertogna (Universita di Modena, Italy)

Abstract:
This paper proposes a solution for the FMTV verification challenge related to the timing and schedulability analysis of an engine management system to be executed on a shared-memory multi-core platform. The application consists of statically partitioned tasks, each one composed of multiple runnables that are executed according to a read-compute-write policy, where the memory labels required by a runnable are loaded from memory before starting its execution, and they are all stored after the runnable completes its execution. Tasks may be either fully preemptive or only partially at runnable boundaries. The contribution of the paper is threefold. First, we present a tight schedulability analysis for this mixed-preemption setting, neglecting memory accesses (Challenge I). Then, memory access times and arbitration delays are included to the schedulability analysis, addressing Challenge II. Finally, Challenge III is tackled proposing different approaches to map the labels to local/global memories so as to minimize the end-to-end latency of selected
event chains.

Attached document:

FMTV_2016_mixed_preemptive.pdf

Statistics: Posted by Sophie Quinton — Fri Jul 01, 2016

Verification challenge • Computational Analysis of Complex Real-Time Systems – FMTV 2016 Verification Challenge

2016-07-01T17:00:14+01:00

Title: Computational Analysis of Complex Real-Time Systems – FMTV 2016 Verification Challenge

Authors:
Ingo Stierand, Philipp Reinkemeier, Sebastian Gerwinn, Thomas Peikenkamp (OFFIS, Oldenburg, Germany)

Abstract:
Real-time scheduling analysis is an important step in safety relevant embedded system design for many application domains, such as avionics, automotive and automation. Increasing system complexity, not least due to raising automated mobility, requires constant evolution of the analysis approaches, resulting in a vital research domain.

We like to contribute to the research by presenting a computational analysis approach, where the system model is unfolded as discrete-time state transition system. The analysis engine is tailored particularly for real-time scheduling analysis and exploits respective optimisations. We show the applicability of the approach on an industrial relevant problem, and discuss its advantages and limits.

Attached document:

FMTV_2016_computational.pdf

Statistics: Posted by Sophie Quinton — Fri Jul 01, 2016

Verification challenge • FMTV 2016: Where is the Actual Challenge?

2016-07-01T16:58:06+01:00

Title: FMTV 2016: Where is the Actual Challenge?

Authors:
Alessio Balsini, Alessandra Melani, Pasquale Buonocunto, Marco Di Natale (Scuola Superiore Sant’Anna, Pisa, Italy)

Abstract: The FMTV challenge has been formulated and proposed to research groups as a case study and benchmark to compare different analysis methods for real-time multicore fuel injection applications. The nature of the problem is clear enough and the challenge can be likely met by a set of conventional analysis techniques (at least at the current level of description). However, the formulation of the problem and its practical solution are more than likely to reveal a number of additional issues that go from the model of the application, to analysis techniques that consider with much better precision the details of the HW platform, to the need for synthesis and optimization methods.

Attached paper:

FMTV_2016_actual_challenge.pdf

Statistics: Posted by Sophie Quinton — Fri Jul 01, 2016

Verification challenge • A Novel Analytical Technique for Timing Analysis of FMTV 2016 Verification Challenge Benchmark

2016-07-01T16:55:09+01:00

Title: A Novel Analytical Technique for Timing Analysis of FMTV 2016 Verification Challenge Benchmark

Authors:
Junchul Choi, Donghyun Kang, and Soonhoi Ha (Department of Computer Science and Engineering, Seoul National University, Korea)

Abstract: In this paper, we present solutions to FMTV 2016 verification challenges, combining the response time analysis and schedule time bound analysis. The worst case response time of a task is computed by the conventional response time analysis while the end-to-end latency of a cause-effect chain is conservatively estimated by considering the schedule time bounds of associated runnables. Three separate challenges are discussed in order. The proposed technique is first explained to address the first challenge that ignores the memory latency. For the second challenge, we estimate the memory access latency by computing the maximum possible arbitration delay with arrival curve analysis. Finally, we propose a heuristic algorithm that determines the mapping of data labels to optimize the end-to-end latency.

Attached paper:

FMTV_2016_analytical.pdf

Statistics: Posted by Sophie Quinton — Fri Jul 01, 2016

Verification challenge • Calculating Latencies in an Engine Management System Using Response Time Analysis with MAST

2016-07-01T16:52:13+01:00

Title: Calculating Latencies in an Engine Management System Using Response Time Analysis with MAST

Authors:
Juan M. Rivas, J. Javier Gutiérrez, Julio L. Medina and Michael González Harbour (Software Engineering and Real-Time Group, University of Cantabria, Spain)

Abstract:
This paper reports solutions to the 2016 edition of the Formal Methods and Timing Verification (FMTV) challenge. The challenge requests calculating latencies in a complex engine management system, of which an Amalthea model is provided. We propose solving the challenge using MAST, which is a real-time systems model and also a suite of tools for schedulability analysis and optimization. The efforts to solve the challenge are mainly focused on translating the Amalthea model into the MAST model. Then, response time schedulability analysis tools are used. We discuss the strengths and limitations of our approach, and present the results obtained. Finally, we report the time needed to understand and complete the challenge. The solutions are available to the public in electronic form to facilitate their assessment by the community.

Attached paper:

FMTV_2016_MAST.pdf

Statistics: Posted by Sophie Quinton — Fri Jul 01, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-20T07:48:53+01:00

Thanks Arne, I think I understand the problem enough to tackle it.

When I analyzed the worst case end-to-end latencies of tasks and chains, too many tasks, 6 out of 21 tasks from my result, violate deadlines even without memory access delay. Chains that have runnables in unschedulable tasks are of course unanalyzable. I'm not sure this unschedulable results have meaning on the challenge, making challenge results not comparable.

Is it OK to leave them unschedulable or should I have to do something like changing some periods to make the whole system schedulable?

Thanks,
Junchul

Hi Junchul,

I would suggest to scale the execution times of the runnables in those tasks, and try to answer the question "What is the maximum execution time for those tasks leading to a schedulable system"?

Arne

Statistics: Posted by arne.hamann — Fri May 20, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-20T07:22:41+01:00

Thanks Arne, I think I understand the problem enough to tackle it.

When I analyzed the worst case end-to-end latencies of tasks and chains, too many tasks, 6 out of 21 tasks from my result, violate deadlines even without memory access delay. Chains that have runnables in unschedulable tasks are of course unanalyzable. I'm not sure this unschedulable results have meaning on the challenge, making challenge results not comparable.

Is it OK to leave them unschedulable or should I have to do something like changing some periods to make the whole system schedulable?

Thanks,
Junchul

Statistics: Posted by hinomk2 — Fri May 20, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-19T11:51:24+01:00

Hello Arne,

3. Very good question. Right, arbitration is done at the memory, we assume no contention on the crossbar. Actually, we forgot to specify the split in access time between crossbar and memory. So your guess is right: take 8 cycles as transfer delay and 1 cycle for each access.

So 8 cycles of transfer delay is for the round trip, that is, 4 "to" and 4 "back from" the memory, is this right?

Thanks,

Nacho.

Statistics: Posted by Nacho_S — Thu May 19, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-19T08:29:51+01:00

Hi, thanks arne for the previous answers.

I have another questions on the memory access model:

1. What happens if preemptive task with higher priority is requested during a resource access of lower priority task? Is the preemptive task blocked until the resource access of lower priority task finishes?

2. Should be a label stored in the local memory when it is fetched from global memory? If my guess is right, total access delay is 9 (to global memory) plus 1 (to local memory). Or is there a temporal storage (such as stack memory area) in a core to store labels for runnable execution?

3. The crossbar has full connectivity. So I guess there is no contention on the crossbar. Then for challenge 2 and 3, the access delay on the memory should be known to compute the arbitration delay, but the access delay in the description seems to include not only memory access delay but also crossbar transfer delay. I guess pure memory access delay is 1 cycle for local/global memory and 8 cycles are crossbar transfer delay, since the cores are symmetric and remote local memory access consists of transfer delay and local memory access delay. Am I right?
For example, suppose a runnable tries to access a label in global memory and there are two access requests in FIFO queue. Then access arbitration delay is 3*9 (9 cycles per each access) if memory access takes 9 cycles. If my guess is right, access arbitration delay is 8(transfer delay) + 3*1(1 cycle per each access).

1. The lower priority finishes its memory access and is only then preempted.

2. There is no local buffering. The data is fetched from global memory and stored into a register. Each access requires thus the full access delay again.

3. Very good question. Right, arbitration is done at the memory, we assume no contention on the crossbar. Actually, we forgot to specify the split in access time between crossbar and memory. So your guess is right: take 8 cycles as transfer delay and 1 cycle for each access.

Statistics: Posted by arne.hamann — Thu May 19, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-16T05:11:15+01:00

Hi, thanks arne for the previous answers.

I have another questions on the memory access model:

1. What happens if preemptive task with higher priority is requested during a resource access of lower priority task? Is the preemptive task blocked until the resource access of lower priority task finishes?

2. Should be a label stored in the local memory when it is fetched from global memory? If my guess is right, total access delay is 9 (to global memory) plus 1 (to local memory). Or is there a temporal storage (such as stack memory area) in a core to store labels for runnable execution?

3. The crossbar has full connectivity. So I guess there is no contention on the crossbar. Then for challenge 2 and 3, the access delay on the memory should be known to compute the arbitration delay, but the access delay in the description seems to include not only memory access delay but also crossbar transfer delay. I guess pure memory access delay is 1 cycle for local/global memory and 8 cycles are crossbar transfer delay, since the cores are symmetric and remote local memory access consists of transfer delay and local memory access delay. Am I right?
For example, suppose a runnable tries to access a label in global memory and there are two access requests in FIFO queue. Then access arbitration delay is 3*9 (9 cycles per each access) if memory access takes 9 cycles. If my guess is right, access arbitration delay is 8(transfer delay) + 3*1(1 cycle per each access).

Statistics: Posted by hinomk2 — Mon May 16, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-12T16:06:19+01:00

Thanks for the response,

I got some new questions:

- With regard to challenge 1: "ignoring memory accesses" means that the fetching of data in the reading/write phases takes "0" time?
- With regard to challenge 2 when read/write time is not neglected: what happens if a task/runnable/core reads the same label multiple time from GRAM? Does it always pay the same penalty for the access to GRAM, or is there any caching effect? (for example, the data is brought to LRAM the first time, so that successive read/write take less time)

Thanks,

Nacho

Dear Nacho,

here are your answers:
1) yes ;-)
2) There is no caching. Conflicts are arbitrated in a FIFO manner as explained above. The data mapping to LRAM and GRAM is static.

I hope that helps,
Arne

Statistics: Posted by arne.hamann — Thu May 12, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-11T17:22:25+01:00

Hi,

I have a question for a given amalthea challenge model.

I started to analyze tasks in model and got a mysterious result.

I added all runnables' upper execution time in Task_10ms, which deadline is 2,000,000 cycles ( 0.01 * 200Mhz), Surprisingly it becomes 2,342,546 cycles in total.

I understood that it means Task_10ms overflows in worst case execution without considering other tasks.

than do I have to analyze it 'mean' execution time? (e.g. lower:452 upper:1782 mean: 979, use 979 to analyze)

or did I analyze model in a wrong way?

I'll wait for your answer :)

Thanks,

Donghyun

Statistics: Posted by kangdongh — Wed May 11, 2016

Verification challenge • Re: The FMTV'16 Challenge

2016-05-06T13:58:16+01:00

Thanks for the response,

I got some new questions:

- With regard to challenge 1: "ignoring memory accesses" means that the fetching of data in the reading/write phases takes "0" time?
- With regard to challenge 2 when read/write time is not neglected: what happens if a task/runnable/core reads the same label multiple time from GRAM? Does it always pay the same penalty for the access to GRAM, or is there any caching effect? (for example, the data is brought to LRAM the first time, so that successive read/write take less time)

Thanks,

Nacho

Statistics: Posted by Nacho_S — Fri May 06, 2016