*banner
 

Stack Size Analysis for Interrupt-driven Programs
Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Tom Henzinger, Jens Palsbert

Citation
Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Tom Henzinger, Jens Palsbert. "Stack Size Analysis for Interrupt-driven Programs". Proceedings of the 10th international conference on Static analysis (SAS'03), 2003.

Abstract
We study the problem of determining stack boundedness and the exact maximum stack size for three classes of interrupt-driven programs. Interrupt-driven programs are used in many real-time applications that require responsive interrupt handling. In order to ensure responsiveness, programmers often enable interrupt processing in the body of lower-priority interrupt handlers. In such programs a programming error can allow interrupt handlers to be interrupted in cyclic fashion to lead to an unbounded stack, causing the system to crash. For a restricted class of interrupt-driven programs, we show that there is a polynomial-time procedure to check stack boundedness, while determining the exact maximum stack size is PSPACE-complete. For a larger class of programs, the two problems are both PSPACE-complete, and for the largest class of programs we consider, the two problems are PSPACE-hard and can be solved in exponential time.

Electronic downloads

Citation formats  
  • HTML
    Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Tom
    Henzinger, Jens Palsbert. <a
    href="http://chess.eecs.berkeley.edu/pubs/730.html"
    >Stack Size Analysis for Interrupt-driven
    Programs</a>, Proceedings of the 10th international
    conference on Static analysis (SAS'03), 2003.
  • Plain text
    Krishnendu Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, Tom
    Henzinger, Jens Palsbert. "Stack Size Analysis for
    Interrupt-driven Programs". Proceedings of the 10th
    international conference on Static analysis (SAS'03), 2003.
  • BibTeX
    @inproceedings{ChatterjeeMaMajumdarZhaoHenzingerPalsbert03_StackSizeAnalysisForInterruptdrivenPrograms,
        author = {Krishnendu Chatterjee and Di Ma and Rupak Majumdar
                  and Tian Zhao and Tom Henzinger and Jens Palsbert},
        title = {Stack Size Analysis for Interrupt-driven Programs},
        booktitle = {Proceedings of the 10th international conference
                  on Static analysis (SAS'03)},
        year = {2003},
        abstract = {We study the problem of determining stack
                  boundedness and the exact maximum stack size for
                  three classes of interrupt-driven programs.
                  Interrupt-driven programs are used in many
                  real-time applications that require responsive
                  interrupt handling. In order to ensure
                  responsiveness, programmers often enable interrupt
                  processing in the body of lower-priority interrupt
                  handlers. In such programs a programming error can
                  allow interrupt handlers to be interrupted in
                  cyclic fashion to lead to an unbounded stack,
                  causing the system to crash. For a restricted
                  class of interrupt-driven programs, we show that
                  there is a polynomial-time procedure to check
                  stack boundedness, while determining the exact
                  maximum stack size is PSPACE-complete. For a
                  larger class of programs, the two problems are
                  both PSPACE-complete, and for the largest class of
                  programs we consider, the two problems are
                  PSPACE-hard and can be solved in exponential time.},
        URL = {http://chess.eecs.berkeley.edu/pubs/730.html}
    }
    

Posted by Christopher Brooks on 4 Nov 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess