GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks
Efficient model checking is important in order to make this type of software verification useful for systems that are complex in their structure. If a system is too large or complex then model checking does not simply scale, i.e., it could take too much time to verify the system. This is one strong...
Main Authors: | , |
---|---|
Format: | Others |
Language: | English |
Published: |
Mälardalens högskola, Akademin för innovation, design och teknik
2012
|
Subjects: | |
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-14661 |
id |
ndltd-UPSALLA1-oai-DiVA.org-mdh-14661 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UPSALLA1-oai-DiVA.org-mdh-146612013-01-08T13:52:20ZGPU-accelerated Model Checking of Periodic Self-Suspending Real-Time TasksengLiberg, TimMåhl, Per-ErikMälardalens högskola, Akademin för innovation, design och teknikMälardalens högskola, Akademin för innovation, design och teknik2012GPUModel CheckingVerificationCUDASTSTree searchGPGPUPeriodic Self-Suspending TasksReal-TimeSchedulingTimed automataEfficient model checking is important in order to make this type of software verification useful for systems that are complex in their structure. If a system is too large or complex then model checking does not simply scale, i.e., it could take too much time to verify the system. This is one strong argument for focusing on making model checking faster. Another interesting aim is to make model checking so fast that it can be used for predicting scheduling decisions for real-time schedulers at runtime. This of course requires the model checking to complete within a order of milliseconds or even microseconds. The aim is set very high but the results of this thesis will at least give a hint on whether this seems possible or not. The magic card for (maybe) making this possible is called Graphics Processing Unit (GPU). This thesis will investigate if and how a model checking algorithm can be ported and executed on a GPU. Modern GPU architectures offers a high degree of processing power since they are equipped with up to 1000 (NVIDIA GTX 590) or 3000 (NVIDIA Tesla K10) processor cores. The drawback is that they offer poor thread-communication possibilities and memory caches compared to CPU. This makes it very difficult to port CPU programs to GPUs.The example model (system) used in this thesis represents a real-time task scheduler that can schedule up to three periodic self-suspending tasks. The aim is to verify, i.e., find a feasible schedule for these tasks, and do it as fast as possible with the help of the GPU. Student thesisinfo:eu-repo/semantics/bachelorThesistexthttp://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-14661application/pdfinfo:eu-repo/semantics/openAccess |
collection |
NDLTD |
language |
English |
format |
Others
|
sources |
NDLTD |
topic |
GPU Model Checking Verification CUDA STS Tree search GPGPU Periodic Self-Suspending Tasks Real-Time Scheduling Timed automata |
spellingShingle |
GPU Model Checking Verification CUDA STS Tree search GPGPU Periodic Self-Suspending Tasks Real-Time Scheduling Timed automata Liberg, Tim Måhl, Per-Erik GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
description |
Efficient model checking is important in order to make this type of software verification useful for systems that are complex in their structure. If a system is too large or complex then model checking does not simply scale, i.e., it could take too much time to verify the system. This is one strong argument for focusing on making model checking faster. Another interesting aim is to make model checking so fast that it can be used for predicting scheduling decisions for real-time schedulers at runtime. This of course requires the model checking to complete within a order of milliseconds or even microseconds. The aim is set very high but the results of this thesis will at least give a hint on whether this seems possible or not. The magic card for (maybe) making this possible is called Graphics Processing Unit (GPU). This thesis will investigate if and how a model checking algorithm can be ported and executed on a GPU. Modern GPU architectures offers a high degree of processing power since they are equipped with up to 1000 (NVIDIA GTX 590) or 3000 (NVIDIA Tesla K10) processor cores. The drawback is that they offer poor thread-communication possibilities and memory caches compared to CPU. This makes it very difficult to port CPU programs to GPUs.The example model (system) used in this thesis represents a real-time task scheduler that can schedule up to three periodic self-suspending tasks. The aim is to verify, i.e., find a feasible schedule for these tasks, and do it as fast as possible with the help of the GPU. |
author |
Liberg, Tim Måhl, Per-Erik |
author_facet |
Liberg, Tim Måhl, Per-Erik |
author_sort |
Liberg, Tim |
title |
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
title_short |
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
title_full |
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
title_fullStr |
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
title_full_unstemmed |
GPU-accelerated Model Checking of Periodic Self-Suspending Real-Time Tasks |
title_sort |
gpu-accelerated model checking of periodic self-suspending real-time tasks |
publisher |
Mälardalens högskola, Akademin för innovation, design och teknik |
publishDate |
2012 |
url |
http://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-14661 |
work_keys_str_mv |
AT libergtim gpuacceleratedmodelcheckingofperiodicselfsuspendingrealtimetasks AT mahlpererik gpuacceleratedmodelcheckingofperiodicselfsuspendingrealtimetasks |
_version_ |
1716531238783680512 |