Effective Candidate Invariant Generation Using GPGPUs and Optimisations

Lloyd-Roberts, Ben; Pantekis, Filippos; James, Phillip; O'Reilly, Liam; Edwards, Mike

doi:10.1109/candar64496.2024.00017

Conference Paper/Proceeding/Abstract 171 views 42 downloads

Effective Candidate Invariant Generation Using GPGPUs and Optimisations

Ben Lloyd-Roberts, Filippos Pantekis

, Phillip James

, Liam O'Reilly

, Mike Edwards

2024 Twelfth International Symposium on Computing and Networking (CANDAR), Pages: 77 - 86

Swansea University Authors: Ben Lloyd-Roberts, Filippos Pantekis , Phillip James , Liam O'Reilly , Mike Edwards

PDF | Accepted Manuscript

Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).
Download (696.1KB)

Check full text

DOI (Published version): 10.1109/candar64496.2024.00017

Abstract

The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states whe...

Full description

Published in:	2024 Twelfth International Symposium on Computing and Networking (CANDAR)
ISBN:	979-8-3315-2837-9 979-8-3315-2836-2
ISSN:	2379-1888 2379-1896
Published:	IEEE 2024
Online Access:	Check full text
URI:	https://cronfa.swan.ac.uk/Record/cronfa68671

first_indexed	2025-01-10T20:24:20Z
last_indexed	2025-02-18T05:39:50Z
id	cronfa68671
recordtype	SURis
fullrecord	<?xml version="1.0"?><rfc1807><datestamp>2025-02-17T11:36:29.4782017</datestamp><bib-version>v2</bib-version><id>68671</id><entry>2025-01-10</entry><title>Effective Candidate Invariant Generation Using GPGPUs and Optimisations</title><swanseaauthors><author><sid>1195fd6c5ca360e99294de541c80587f</sid><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><name>Ben Lloyd-Roberts</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>7e3976bc926b363ee1346c423ba74d11</sid><ORCID>0000-0001-7817-6450</ORCID><firstname>Filippos</firstname><surname>Pantekis</surname><name>Filippos Pantekis</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>fd3b15ff96c5ea91a100131abac558b6</sid><ORCID>0000-0002-4307-649X</ORCID><firstname>Phillip</firstname><surname>James</surname><name>Phillip James</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5eca7cf79b7384130a1feef384d90508</sid><ORCID>0000-0002-4894-2158</ORCID><firstname>Liam</firstname><surname>O'Reilly</surname><name>Liam O'Reilly</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>684864a1ce01c3d774e83ed55e41770e</sid><ORCID>0000-0003-3367-969X</ORCID><firstname>Mike</firstname><surname>Edwards</surname><name>Mike Edwards</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-01-10</date><deptcode>MACS</deptcode><abstract>The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states where safety conditions are violated by transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over-approximation of reachable states, excluding transitions from safe to unsafe states, remove these false positives. However, such invariants are difficult to deduce automatically. This paper advances existing work on using reinforcement learning (RL) and correlation measures to generate candidate invariants. This entails mapping programs to an RL environment, incentivising agents to explore state spaces and analysing observations for invariant patterns. We observe certain complications surrounding the computation of these correlation coefficients when processing large industrial programs. This paper presents our approach using General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges. We detail the steps taken to optimise our GPU kernel and present results on tested devices and inputs. We achieve runtime performance orders of magnitude higher than multi- and single-threaded CPU-side implementations, with speedups ranging from ≈21× to ≈318× when generating correlation coefficients for producing candidate invariants.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>2024 Twelfth International Symposium on Computing and Networking (CANDAR)</journal><volume>0</volume><journalNumber/><paginationStart>77</paginationStart><paginationEnd>86</paginationEnd><publisher>IEEE</publisher><placeOfPublication/><isbnPrint>979-8-3315-2837-9</isbnPrint><isbnElectronic>979-8-3315-2836-2</isbnElectronic><issnPrint>2379-1888</issnPrint><issnElectronic>2379-1896</issnElectronic><keywords>Correlation coefficient, Performance evaluation, Runtime, Graphics processing units, Reinforcement learning, Model checking, Rail transportation, Safety, Space Space exploration, Optimization, formal verification, invariant finding, massively parallel, kernel optimisations</keywords><publishedDay>26</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-11-26</publishedDate><doi>10.1109/candar64496.2024.00017</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm>Not Required</apcterm><funders>Ben Lloyd-Roberts is funded by the EPSRC Centre for Doctoral Training in Enhancing Human Interactions and Collaborations with Data and Intelligence Driven Systems (EP/S021892/1) and Siemens Mobility UK.</funders><projectreference>EP/S021892/1</projectreference><lastEdited>2025-02-17T11:36:29.4782017</lastEdited><Created>2025-01-10T13:28:27.8095082</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ben</firstname><surname>Lloyd-Roberts</surname><order>1</order></author><author><firstname>Filippos</firstname><surname>Pantekis</surname><orcid>0000-0001-7817-6450</orcid><order>2</order></author><author><firstname>Phillip</firstname><surname>James</surname><orcid>0000-0002-4307-649X</orcid><order>3</order></author><author><firstname>Liam</firstname><surname>O'Reilly</surname><orcid>0000-0002-4894-2158</orcid><order>4</order></author><author><firstname>Mike</firstname><surname>Edwards</surname><orcid>0000-0003-3367-969X</orcid><order>5</order></author></authors><documents><document><filename>68671__33560__1825d968995344fbbc628629e8fc4000.pdf</filename><originalFilename>CANDAR_24.pdf</originalFilename><uploaded>2025-02-11T13:36:20.8685765</uploaded><type>Output</type><contentLength>712811</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><documentNotes>Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>English</language><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling	2025-02-17T11:36:29.4782017 v2 68671 2025-01-10 Effective Candidate Invariant Generation Using GPGPUs and Optimisations 1195fd6c5ca360e99294de541c80587f Ben Lloyd-Roberts Ben Lloyd-Roberts true false 7e3976bc926b363ee1346c423ba74d11 0000-0001-7817-6450 Filippos Pantekis Filippos Pantekis true false fd3b15ff96c5ea91a100131abac558b6 0000-0002-4307-649X Phillip James Phillip James true false 5eca7cf79b7384130a1feef384d90508 0000-0002-4894-2158 Liam O'Reilly Liam O'Reilly true false 684864a1ce01c3d774e83ed55e41770e 0000-0003-3367-969X Mike Edwards Mike Edwards true false 2025-01-10 MACS The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states where safety conditions are violated by transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over-approximation of reachable states, excluding transitions from safe to unsafe states, remove these false positives. However, such invariants are difficult to deduce automatically. This paper advances existing work on using reinforcement learning (RL) and correlation measures to generate candidate invariants. This entails mapping programs to an RL environment, incentivising agents to explore state spaces and analysing observations for invariant patterns. We observe certain complications surrounding the computation of these correlation coefficients when processing large industrial programs. This paper presents our approach using General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges. We detail the steps taken to optimise our GPU kernel and present results on tested devices and inputs. We achieve runtime performance orders of magnitude higher than multi- and single-threaded CPU-side implementations, with speedups ranging from ≈21× to ≈318× when generating correlation coefficients for producing candidate invariants. Conference Paper/Proceeding/Abstract 2024 Twelfth International Symposium on Computing and Networking (CANDAR) 0 77 86 IEEE 979-8-3315-2837-9 979-8-3315-2836-2 2379-1888 2379-1896 Correlation coefficient, Performance evaluation, Runtime, Graphics processing units, Reinforcement learning, Model checking, Rail transportation, Safety, Space Space exploration, Optimization, formal verification, invariant finding, massively parallel, kernel optimisations 26 11 2024 2024-11-26 10.1109/candar64496.2024.00017 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Not Required Ben Lloyd-Roberts is funded by the EPSRC Centre for Doctoral Training in Enhancing Human Interactions and Collaborations with Data and Intelligence Driven Systems (EP/S021892/1) and Siemens Mobility UK. EP/S021892/1 2025-02-17T11:36:29.4782017 2025-01-10T13:28:27.8095082 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ben Lloyd-Roberts 1 Filippos Pantekis 0000-0001-7817-6450 2 Phillip James 0000-0002-4307-649X 3 Liam O'Reilly 0000-0002-4894-2158 4 Mike Edwards 0000-0003-3367-969X 5 68671__33560__1825d968995344fbbc628629e8fc4000.pdf CANDAR_24.pdf 2025-02-11T13:36:20.8685765 Output 712811 application/pdf Accepted Manuscript true Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention). true English https://creativecommons.org/licenses/by/4.0/
title	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
spellingShingle	Effective Candidate Invariant Generation Using GPGPUs and Optimisations Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
title_short	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
title_full	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
title_fullStr	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
title_full_unstemmed	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
title_sort	Effective Candidate Invariant Generation Using GPGPUs and Optimisations
author_id_str_mv	1195fd6c5ca360e99294de541c80587f 7e3976bc926b363ee1346c423ba74d11 fd3b15ff96c5ea91a100131abac558b6 5eca7cf79b7384130a1feef384d90508 684864a1ce01c3d774e83ed55e41770e
author_id_fullname_str_mv	1195fd6c5ca360e99294de541c80587f_*_Ben Lloyd-Roberts 7e3976bc926b363ee1346c423ba74d11__Filippos Pantekis fd3b15ff96c5ea91a100131abac558b6__Phillip James 5eca7cf79b7384130a1feef384d90508__Liam O'Reilly 684864a1ce01c3d774e83ed55e41770e_**_Mike Edwards
author	Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
author2	Ben Lloyd-Roberts Filippos Pantekis Phillip James Liam O'Reilly Mike Edwards
format	Conference Paper/Proceeding/Abstract
container_title	2024 Twelfth International Symposium on Computing and Networking (CANDAR)
container_volume	0
container_start_page	77
publishDate	2024
institution	Swansea University
isbn	979-8-3315-2837-9 979-8-3315-2836-2
issn	2379-1888 2379-1896
doi_str_mv	10.1109/candar64496.2024.00017
publisher	IEEE
college_str	Faculty of Science and Engineering
hierarchytype
hierarchy_top_id	facultyofscienceandengineering
hierarchy_top_title	Faculty of Science and Engineering
hierarchy_parent_id	facultyofscienceandengineering
hierarchy_parent_title	Faculty of Science and Engineering
department_str	School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str	1
active_str	0
description	The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states where safety conditions are violated by transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over-approximation of reachable states, excluding transitions from safe to unsafe states, remove these false positives. However, such invariants are difficult to deduce automatically. This paper advances existing work on using reinforcement learning (RL) and correlation measures to generate candidate invariants. This entails mapping programs to an RL environment, incentivising agents to explore state spaces and analysing observations for invariant patterns. We observe certain complications surrounding the computation of these correlation coefficients when processing large industrial programs. This paper presents our approach using General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges. We detail the steps taken to optimise our GPU kernel and present results on tested devices and inputs. We achieve runtime performance orders of magnitude higher than multi- and single-threaded CPU-side implementations, with speedups ranging from ≈21× to ≈318× when generating correlation coefficients for producing candidate invariants.
published_date	2024-11-26T14:02:32Z
_version_	1831919895637393408
score	11.0588665

Effective Candidate Invariant Generation Using GPGPUs and Optimisations

Similar Items