Bottleneck analysis of a gigabit network interface card: Formal verification approach

Hyun Wook Jin, Ki Seok Bang, Hyuck Yoo, Jin Young Choi, Ho Jung Cha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

This paper addresses how formal verification can be applied to find a bottleneck in a gigabit network interface card that prevents the card from achieving the best possible performance. Finding a bottleneck in a gigabit network interface card is not an easy task because it is equipped with sophisticated hardware components, such as multiple DMA engines and separate CPU and memory. Therefore, the interactions between a network interface card and the host are very complex so that the firmware to manage the interactions is also complicated, which makes the bottleneck analysis very difficult. As an alternative approach of the bottleneck analysis, we specify the firmware in a gigabit network interface card and analyze the behavior of the specification with SPIN. As an example of gigabit network interface cards, Myrinet is used in this paper. We show that SPIN can easily verify whether the Myrinet firmware has a bottleneck once the state transitions inside the firmware are modeled properly.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages170-186
Number of pages17
Volume2318 LNCS
ISBN (Print)3540434771, 9783540434771
Publication statusPublished - 2002 Jan 1
Event9th International SPIN Workshop on Model Checking Software, SPIN 2002 - Grenoble, France
Duration: 2002 Apr 112002 Apr 13

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2318 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International SPIN Workshop on Model Checking Software, SPIN 2002
CountryFrance
CityGrenoble
Period02/4/1102/4/13

Fingerprint

Formal Verification
Firmware
Interfaces (computer)
Dynamic mechanical analysis
State Transition
Interaction
Program processors
Engine
Formal verification
Hardware
Specification
Verify
Engines
Specifications
Data storage equipment
Alternatives

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Jin, H. W., Bang, K. S., Yoo, H., Choi, J. Y., & Cha, H. J. (2002). Bottleneck analysis of a gigabit network interface card: Formal verification approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2318 LNCS, pp. 170-186). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2318 LNCS). Springer Verlag.

Bottleneck analysis of a gigabit network interface card : Formal verification approach. / Jin, Hyun Wook; Bang, Ki Seok; Yoo, Hyuck; Choi, Jin Young; Cha, Ho Jung.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2318 LNCS Springer Verlag, 2002. p. 170-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2318 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Jin, HW, Bang, KS, Yoo, H, Choi, JY & Cha, HJ 2002, Bottleneck analysis of a gigabit network interface card: Formal verification approach. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 2318 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2318 LNCS, Springer Verlag, pp. 170-186, 9th International SPIN Workshop on Model Checking Software, SPIN 2002, Grenoble, France, 02/4/11.
Jin HW, Bang KS, Yoo H, Choi JY, Cha HJ. Bottleneck analysis of a gigabit network interface card: Formal verification approach. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2318 LNCS. Springer Verlag. 2002. p. 170-186. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Jin, Hyun Wook ; Bang, Ki Seok ; Yoo, Hyuck ; Choi, Jin Young ; Cha, Ho Jung. / Bottleneck analysis of a gigabit network interface card : Formal verification approach. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2318 LNCS Springer Verlag, 2002. pp. 170-186 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{76ad145d163a4d1ea2475d8f0ffd85df,
title = "Bottleneck analysis of a gigabit network interface card: Formal verification approach",
abstract = "This paper addresses how formal verification can be applied to find a bottleneck in a gigabit network interface card that prevents the card from achieving the best possible performance. Finding a bottleneck in a gigabit network interface card is not an easy task because it is equipped with sophisticated hardware components, such as multiple DMA engines and separate CPU and memory. Therefore, the interactions between a network interface card and the host are very complex so that the firmware to manage the interactions is also complicated, which makes the bottleneck analysis very difficult. As an alternative approach of the bottleneck analysis, we specify the firmware in a gigabit network interface card and analyze the behavior of the specification with SPIN. As an example of gigabit network interface cards, Myrinet is used in this paper. We show that SPIN can easily verify whether the Myrinet firmware has a bottleneck once the state transitions inside the firmware are modeled properly.",
author = "Jin, {Hyun Wook} and Bang, {Ki Seok} and Hyuck Yoo and Choi, {Jin Young} and Cha, {Ho Jung}",
year = "2002",
month = "1",
day = "1",
language = "English",
isbn = "3540434771",
volume = "2318 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "170--186",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Bottleneck analysis of a gigabit network interface card

T2 - Formal verification approach

AU - Jin, Hyun Wook

AU - Bang, Ki Seok

AU - Yoo, Hyuck

AU - Choi, Jin Young

AU - Cha, Ho Jung

PY - 2002/1/1

Y1 - 2002/1/1

N2 - This paper addresses how formal verification can be applied to find a bottleneck in a gigabit network interface card that prevents the card from achieving the best possible performance. Finding a bottleneck in a gigabit network interface card is not an easy task because it is equipped with sophisticated hardware components, such as multiple DMA engines and separate CPU and memory. Therefore, the interactions between a network interface card and the host are very complex so that the firmware to manage the interactions is also complicated, which makes the bottleneck analysis very difficult. As an alternative approach of the bottleneck analysis, we specify the firmware in a gigabit network interface card and analyze the behavior of the specification with SPIN. As an example of gigabit network interface cards, Myrinet is used in this paper. We show that SPIN can easily verify whether the Myrinet firmware has a bottleneck once the state transitions inside the firmware are modeled properly.

AB - This paper addresses how formal verification can be applied to find a bottleneck in a gigabit network interface card that prevents the card from achieving the best possible performance. Finding a bottleneck in a gigabit network interface card is not an easy task because it is equipped with sophisticated hardware components, such as multiple DMA engines and separate CPU and memory. Therefore, the interactions between a network interface card and the host are very complex so that the firmware to manage the interactions is also complicated, which makes the bottleneck analysis very difficult. As an alternative approach of the bottleneck analysis, we specify the firmware in a gigabit network interface card and analyze the behavior of the specification with SPIN. As an example of gigabit network interface cards, Myrinet is used in this paper. We show that SPIN can easily verify whether the Myrinet firmware has a bottleneck once the state transitions inside the firmware are modeled properly.

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

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

M3 - Conference contribution

AN - SCOPUS:84893630480

SN - 3540434771

SN - 9783540434771

VL - 2318 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 170

EP - 186

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -