Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics

Sanne Wouda; Sebastiaan J.C. Joosten; Julien Schmaltz

doi:10.1109/MEMCOD.2015.7340487

Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics

Sanne Wouda, Sebastiaan J.C. Joosten, Julien Schmaltz

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

Abstract

We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

Original language	English
Title of host publication	2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015
Publisher	Institute of Electrical and Electronics Engineers
Pages	198-207
Number of pages	10
ISBN (Electronic)	9781509002375
DOIs	https://doi.org/10.1109/MEMCOD.2015.7340487
Publication status	Published - 30 Nov 2015
Event	ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015) - Austin, United States Duration: 21 Sep 2015 → 23 Sep 2015

Conference

Conference	ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015)
Abbreviated title	MEMOCODE 2015
Country/Territory	United States
City	Austin
Period	21/09/15 → 23/09/15

Keywords

Algebra
Computational modeling
Fabrics
Ports (Computers)
Reachability analysis
Semantics
System recovery

Access to Document

10.1109/MEMCOD.2015.7340487

Cite this

Wouda, S., Joosten, S. J. C., & Schmaltz, J. (2015). Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics. In 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015 (pp. 198-207). [7340487] Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/MEMCOD.2015.7340487

@inproceedings{1cba3f2b3cc84cef8ffcd38ee1d6a7d8,

title = "Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics",

abstract = "We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.",

keywords = "Algebra, Computational modeling, Fabrics, Ports (Computers), Reachability analysis, Semantics, System recovery",

author = "Sanne Wouda and Joosten, {Sebastiaan J.C.} and Julien Schmaltz",

year = "2015",

month = nov,

day = "30",

doi = "10.1109/MEMCOD.2015.7340487",

language = "English",

pages = "198--207",

booktitle = "2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015), MEMOCODE 2015 ; Conference date: 21-09-2015 Through 23-09-2015",

}

Wouda, S, Joosten, SJC & Schmaltz, J 2015, Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics. in 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015., 7340487, Institute of Electrical and Electronics Engineers, pp. 198-207, ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015), Austin, United States, 21/09/15. https://doi.org/10.1109/MEMCOD.2015.7340487

Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics. / Wouda, Sanne; Joosten, Sebastiaan J.C.; Schmaltz, Julien.

2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015. Institute of Electrical and Electronics Engineers, 2015. p. 198-207 7340487.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics

AU - Wouda, Sanne

AU - Joosten, Sebastiaan J.C.

AU - Schmaltz, Julien

PY - 2015/11/30

Y1 - 2015/11/30

N2 - We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

AB - We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

KW - Algebra

KW - Computational modeling

KW - Fabrics

KW - Ports (Computers)

KW - Reachability analysis

KW - Semantics

KW - System recovery

UR - http://www.scopus.com/inward/record.url?scp=84960968072&partnerID=8YFLogxK

U2 - 10.1109/MEMCOD.2015.7340487

DO - 10.1109/MEMCOD.2015.7340487

M3 - Conference contribution

AN - SCOPUS:84960968072

SP - 198

EP - 207

BT - 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015

PB - Institute of Electrical and Electronics Engineers

T2 - ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2015)

Y2 - 21 September 2015 through 23 September 2015

ER -

Process algebra semantics & reachability analysis for micro-architectural models of communication fabrics

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this