liu.seSearch for publications in DiVA
Change search
Link to record
Permanent link

Direct link
Alternative names
Publications (10 of 20) Show all publications
Horga, A., Rezine, A., Chattopadhyay, S., Eles, P. I. & Peng, Z. (2022). Symbolic identification of shared memory based bank conflicts for GPUs. Journal of systems architecture, 127, Article ID 102518.
Open this publication in new window or tab >>Symbolic identification of shared memory based bank conflicts for GPUs
Show others...
2022 (English)In: Journal of systems architecture, ISSN 1383-7621, E-ISSN 1873-6165, Vol. 127, article id 102518Article in journal (Refereed) Published
Abstract [en]

Graphic processing units (GPUs) are routinely used for general purpose computations to improve performance. To achieve the sought performance gains, care must be invested in fine tuning the way GPU programs interact with the underlying architecture, accounting for the shared memory bank conflicts and the entailed shared memory transactions. Uncovering inputs leading to particular bank conflicts can turn out to be quite hard given the intricacy of the access patterns and their dependence on the inputs. We propose a symbolic execution based framework to systematically uncover shared memory bank conflicts, to propose inputs to realize a given number of shared memory transactions, and to refute the existence of such inputs if the number of shared memory transactions is impossible to achieve during the execution. This allows programmers to more formally reason about the shared memory conflicts and to validate their impact on performance and security. We have implemented our approach and report on our experiments to explore its usefulness towards performance enhancement and quantifying shared memory side-channel leakage in security applications.

Place, publisher, year, edition, pages
Amsterdam, Netherlands: Elsevier, 2022
Keywords
GPU; Shared memory; Formal verification; Performance evaluation; Software security
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-184473 (URN)10.1016/j.sysarc.2022.102518 (DOI)000797269300005 ()
Note

Funding: Swedish Research Council [2017-04194, 2018-05973]; Singapore Ministry of Education (MOE) [MOE2018-T2-1-098]; National Research Foundation (NRF) [NRF2019-NRF-ANR092]

Available from: 2022-04-22 Created: 2022-04-22 Last updated: 2022-06-08Bibliographically approved
Mahfouzi, R., Aminifar, A., Samii, S., Rezine, A., Eles, P. & Peng, Z. (2021). Breaking Silos to Guarantee Control Stability with Communication over Ethernet TSN. IEEE design & test, 38(5), 48-56
Open this publication in new window or tab >>Breaking Silos to Guarantee Control Stability with Communication over Ethernet TSN
Show others...
2021 (English)In: IEEE design & test, ISSN 2168-2356, E-ISSN 2168-2364, ISSN 2168-2356, Vol. 38, no 5, p. 48-56Article in journal (Refereed) Published
Abstract [en]

This article presents a methodology for cross-layer control–communication co-synthesis of cyber-physical systems (CPSs), communicating over Ethernet networks, with stability guarantees. We consider the recently developed IEEE 802.1 Time-Sensitive Networking standards for real-time Ethernet communication, in particular 802.1Qbv-2015, which is gaining traction in automotive and industrial automation applications. Specifically, we address routing and static scheduling of Ethernet control packets in a CPS with a switched Ethernet communication network connecting sensors, computers, and actuators. The design problem spans the network and control application layers. Our proposed SMT-based solution integrates many decision variables and objectives related to message routing, scheduling, and control application stability.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2021
Keywords
Embedded Control Systems, Real-Time Control Systems, Cyber-Physical Systems, Automotive Systems, Control-Scheduling Co-Design, Stability-Aware Design, Integrated Routing and Scheduling, Ethernet Networks
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-164267 (URN)10.1109/MDAT.2020.2968281 (DOI)000701241400013 ()2-s2.0-85078087581 (Scopus ID)
Available from: 2020-03-13 Created: 2020-03-13 Last updated: 2023-01-09Bibliographically approved
Ganjei, Z., Rezine, A., Eles, P. I. & Peng, Z. (2021). Verifying Safety of Parameterized Heard-Of Algorithms. In: Chryssis Georgiou and Rupak Majumdar (Ed.), : . Paper presented at  Networked Systems. 8th International Conference, NETYS 2020 (pp. 209-226). Springer, 12129
Open this publication in new window or tab >>Verifying Safety of Parameterized Heard-Of Algorithms
2021 (English)In: / [ed] Chryssis Georgiou and Rupak Majumdar, Springer, 2021, Vol. 12129, p. 209-226Conference paper, Published paper (Refereed)
Abstract [en]

We consider the problem of automatically checking safety properties of fault-tolerant distributed algorithms. We express the considered class of distributed algorithms in terms of the Heard-Of Model where arbitrary many processes proceed in infinite rounds in the presence of failures such as message losses or message corruptions. We propose, for the considered class, a sound but (in general) incomplete procedure that is guaranteed to terminate even in the presence of unbounded numbers of processes. In addition, we report on preliminary experiments for which either correctness is proved by our approach or a concrete trace violating the considered safety property is automatically found.

Place, publisher, year, edition, pages
Springer, 2021
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-175907 (URN)10.1007/978-3-030-67087-0_14 (DOI)978-3-030-67086-3 (ISBN)978-3-030-67087-0 (ISBN)
Conference
 Networked Systems. 8th International Conference, NETYS 2020
Available from: 2021-05-26 Created: 2021-05-26 Last updated: 2022-09-05
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Counting dynamically synchronizing processes. International Journal on Software Tools for Technology Transfer, 18(5), 517-534
Open this publication in new window or tab >>Counting dynamically synchronizing processes
2016 (English)In: International Journal on Software Tools for Technology Transfer, ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, no 5, p. 517-534Article in journal (Refereed) Published
Abstract [en]

We address the problem of automatically establishing correctness for programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. The programs we consider can make use of the shared variables to count and synchronize the spawned processes. This allows them to implement intricate synchronization mechanisms, such as barriers. Automatically verifying correctness, and deadlock freedom, of such programs is beyond the capabilities of current techniques. For this purpose, we make use of counting predicates that mix counters referring to the number of processes satisfying certain properties and variables directly manipulated by the concurrent processes. We then combine existing works on counter, predicate, and constrained monotonic abstraction and build a nested counter example based refinement scheme for establishing correctness (expressed as non-reachability of configurations satisfying counting predicates formulas). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification on several programs whose correctness crucially depends on precisely capturing the number of processes synchronizing using shared variables.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Keywords
Parameterized verification, Counting predicate, Barrier synchronization, Deadlock freedom, Multithreaded programs, Counter abstraction, Predicate abstraction, Constrained monotonic abstraction
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-124406 (URN)10.1007/s10009-015-0411-0 (DOI)000382011100004 ()
Note

Funding agencies: 12.04 CENIIT project

Available from: 2016-01-28 Created: 2016-01-28 Last updated: 2024-01-17
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2016). Lazy Constrained Monotonic Abstraction. In: Barbara Jobstmann; K. Rustan M. Leino (Ed.), Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Paper presented at 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016 (pp. 147-165). Springer Berlin/Heidelberg, 9583
Open this publication in new window or tab >>Lazy Constrained Monotonic Abstraction
2016 (English)In: Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings / [ed] Barbara Jobstmann; K. Rustan M. Leino, Springer Berlin/Heidelberg, 2016, Vol. 9583, p. 147-165Conference paper, Published paper (Refereed)
Abstract [en]

We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349
Keywords
Constrained monotonic abstraction, Lazy exploration, Well structured systems, Safety properties, Counter machines reachability
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-123739 (URN)10.1007/978-3-662-49122-5_7 (DOI)000375148800007 ()9783662491218 (ISBN)9783662491225 (ISBN)
Conference
17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016
Available from: 2016-01-11 Created: 2016-01-11 Last updated: 2018-02-06Bibliographically approved
Ganjei, Z., Rezine, A., Ion Eles, P. & Peng, Z. (2015). Abstracting and Counting Synchronizing Processes. In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015.. Paper presented at VMCAI 15 (pp. 227-244). Springer
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2015 (English)In: Verification, Model Checking, and Abstract Interpretation: 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015), Mumbai, India, Jan. 12-14, 2015., Springer, 2015, p. 227-244Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables referring to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8931
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-114467 (URN)10.1007/978-3-662-46081-8_13 (DOI)000354784200013 ()978-3-662-46080-1 (ISBN)978-3-662-46081-8 (ISBN)
Conference
VMCAI 15
Available from: 2015-02-20 Created: 2015-02-20 Last updated: 2018-01-11
Aziz Abdulla, P., Faouzi Atig, M., Chen, Y.-F., Holik, L., Rezine, A., Rummer, P. & Stenman, J. (2015). Norn: An SMT Solver for String Constraints. In: Kroening, Daniel, Păsăreanu, Corina S. (Ed.), COMPUTER AIDED VERIFICATION, PT I: . Paper presented at 27th International Conference on Computer-Aided Verification (CAV) (pp. 462-469). SPRINGER-VERLAG BERLIN, 9206
Open this publication in new window or tab >>Norn: An SMT Solver for String Constraints
Show others...
2015 (English)In: COMPUTER AIDED VERIFICATION, PT I / [ed] Kroening, Daniel, Păsăreanu, Corina S., SPRINGER-VERLAG BERLIN , 2015, Vol. 9206, p. 462-469Conference paper, Published paper (Refereed)
Abstract [en]

We present version 1.0 of the Norn SMT solver for string constraints. Norn is a solver for an expressive constraint language, including word equations, length constraints, and regular membership queries. As a feature distinguishing Norn from other SMT solvers, Norn is a decision procedure under the assumption of a set of acyclicity conditions on word equations, without any restrictions on the use of regular membership.

Place, publisher, year, edition, pages
SPRINGER-VERLAG BERLIN, 2015
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 9206
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-123090 (URN)10.1007/978-3-319-21690-4_29 (DOI)000364182900029 ()978-3-319-21690-4 (ISBN)978-3-319-21689-8 (ISBN)
Conference
27th International Conference on Computer-Aided Verification (CAV)
Available from: 2015-12-03 Created: 2015-12-03 Last updated: 2018-02-15
Abdulla, P. A., Atig, M. F., Ganjei, Z., Rezine, A. & Zhu, Y. (2015). Verification of Cache Coherence Protocols wrt. Trace Filters. In: : . Paper presented at Formal Methods in Computer-Aided Design (FMCAD). IEEE
Open this publication in new window or tab >>Verification of Cache Coherence Protocols wrt. Trace Filters
Show others...
2015 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of parameterized verification of cache coherence protocols for hardware accelerated transactional memories. In this setting, transactional memories leverage on the versioning capabilities of the underlying cache coherence protocol. The length of the transactions, their number, and the number of manipulated variables (i.e., cache lines) are parameters of the verification problem. Caches in such systems are finite-state automata communicating via broadcasts and shared variables. We augment our system with filters that restrict the set of possible executable traces according to existing conflict resolution policies. We show that the verification of coherence for parameterized cache protocols with filters can be reduced to systems with only a finite number of cache lines. For verification, we show how to account for the effect of the adopted filters in a symbolic backward reachability algorithm based on the framework of constrained monotonic abstraction. We have implemented our method and used it to verify transactional memory coherence protocols with respect to different conflict resolution policies.

Place, publisher, year, edition, pages
IEEE, 2015
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-128860 (URN)9780983567851 (ISBN)
Conference
Formal Methods in Computer-Aided Design (FMCAD)
Available from: 2016-06-02 Created: 2016-06-02 Last updated: 2018-01-10
Ganjei, Z., Rezine, A., Eles, P. & Peng, Z. (2014). Abstracting and Counting Synchronizing Processes.
Open this publication in new window or tab >>Abstracting and Counting Synchronizing Processes
2014 (English)Report (Other academic)
Abstract [en]

We address the problem of automatically establishing synchronization dependent correctness (e.g. due to using barriers or ensuring absence of deadlocks) of programs generating an arbitrary number of concurrent processes and manipulating variables ranging over an infinite domain. Automatically checking such properties for these programs is beyond the capabilities of current verification techniques. For this purpose, we describe an original logic that mixes two sorts of variables: those shared and manipulated by the concurrent processes, and ghost variables refering to the number of processes satisfying predicates on shared and local program variables. We then combine existing works on counter, predicate, and constrained monotonic abstraction and nest two cooperating counter example based refinement loops for establishing correctness (safety expressed as non reachability of configurations satisfying formulas in our logic). We have implemented a tool (Pacman, for predicated constrained monotonic abstraction) and used it to perform parameterized verification for several programs whose correctness crucially depends on precisely capturing the number of synchronizing processes. 

Publisher
p. 35
Series
Technical reports in Computer and Information Science, ISSN 1654-7233
Keywords
Parameterized verification, counting logic, barrier synchronization, deadlock freedom, multithreaded programs, counter abstraction, predicate abstraction, constrained monotonic abstraction
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-111739 (URN)
Available from: 2014-10-30 Created: 2014-10-30 Last updated: 2014-10-31Bibliographically approved
Ganty, P. & Rezine, A. (2014). Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification. In: LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014): . Paper presented at 8th International Conference on Language and Automata Theory and Applications (LATA) (pp. 396-408). Springer Berlin/Heidelberg, 8370
Open this publication in new window or tab >>Ordered Counter-Abstraction Refinable Subword Relations for Parameterized Verification
2014 (English)In: LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), Springer Berlin/Heidelberg, 2014, Vol. 8370, p. 396-408Conference paper, Published paper (Refereed)
Abstract [en]

We present an original refinable subword based symbolic representation for the verification of linearly ordered parameterized systems. Such a system consists of arbitrary many finite processes placed in an array. Processes communicate using global transitions constrained by their relative positions (i.e., priorities). The model can include binary communication, broadcast, shared variables or dynamic creation and deletion of processes. Configurations are finite words of arbitrary lengths. The successful monotonic abstraction approach uses the subword relation to define upward closed sets as symbolic representations for such systems. Natural and automatic refinements remained missing for such symbolic representations. For instance, subword based relations are simply too coarse for automatic forward verification of systems involving priorities. We remedy to this situation and introduce a symbolic representation based on an original combination of counter abstraction with subword based relations. This allows us to define an infinite family of relaxation operators that guarantee termination by a new well quasi ordering argument. The proposed automatic analysis is at least as precise and efficient as monotonic abstraction when performed backwards. It can also be successfully used in forward, something monotonic abstraction is incapable of. We implemented a prototype to illustrate the approach.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2014
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 8370
Keywords
counter abstraction; well quasi ordering; reachability; parameterized verification
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:liu:diva-117675 (URN)10.1007/978-3-319-04921-2_32 (DOI)000352688800032 ()2-s2.0-84898069230 (Scopus ID)978-3-319-04921-2 (ISBN)978-3-319-04920-5 (ISBN)
Conference
8th International Conference on Language and Automata Theory and Applications (LATA)
Available from: 2015-05-11 Created: 2015-05-06 Last updated: 2018-01-31
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-0440-4753

Search in DiVA

Show all publications