- Suche

- Kontakt

Technische Berichte

2012

  • The ForMoSA Approach to Qualitative and Quantitative Model-Based Safety Analysis
    Axel Habermaier, Matthias Güdemann, Frank Ortmeier, Wolfgang Reif, Gerhard Schellhorn
    Railway Safety, Reliability, and Security: Technologies and Systems Engineering
    This chapter presents ForMoSA (FORmal MOdels and Safety Analysis), an integrated approach for the safety assessment of safety-critical embedded systems. The approach brings together the best of engineering practice, formal methods, and mathematics: traditional safety analysis, temporal logics and verification, as well as statistics and optimization. These three orthogonal techniques cover three different aspects of safety: fault tolerance, functional correctness, and quantitative analysis. The ForMoSA approach combines these techniques to assess system safety in a structured and formal way. Furthermore, the tight combination of methods from different analysis domains results in mutual benefits. The combined approach yields results which cannot be produced by any single technique on its own. The methodology was applied to several case studies from different industrial domains. One of them is an autonomous control of level crossings using radio-based communication, which is used in this chapter to describe the individual steps of the ForMoSA methodology.
  • On the Correctness of the SIMT Execution Model of GPUs (ESOP'12 Paper)
    Axel Habermaier, Alexander Knapp
    LNCS 7211
    GPUs are becoming a primary resource of computing power. They use a single instruction, multiple threads (SIMT) execution model that executes batches of threads in lockstep. If the control flow of threads within the same batch diverges, the different execution paths are scheduled sequentially; once the control flows reconverge, all threads are executed in lockstep again. Several thread batching mechanisms have been proposed, albeit without establishing their semantic validity or their scheduling properties. To increase the level of confidence in the correctness of GPU-accelerated programs, we formalize the SIMT execution model for a stack-based reconvergence mechanism in an operational semantics and prove its correctness by constructing a simulation between the SIMT semantics and a standard interleaved multi-thread semantics. We also demonstrate that the SIMT execution model produces unfair schedules in some cases. We discuss the problem of unfairness for different batching mechanisms like dynamic warp formation and a stack-less reconvergence strategy.
  • The Confidence-Probability Semiring implemented within OpenFst
    Markus Huber, Christian Kölbl
    Technical Report, Institute of Computer Science, University of Augsburg, March 2012
    2011-16
  • On the Correctness of the SIMT Execution Model of GPUs (Technical Report)
    Axel Habermaier, Alexander Knapp
    Technical Report 2012-01, Institute of Computer Science, University of Augsburg
    GPUs are becoming a primary resource of computing power. They use a single instruction, multiple threads (SIMT) execution model that executes batches of threads in lockstep. If the control flow of threads within the same batch diverges, the different execution paths are scheduled sequentially; once the control flows reconverge, all threads are executed in lockstep again. Several thread batching mechanisms have been proposed, albeit without establishing their semantic validity or their scheduling properties. To increase the level of confidence in the correctness of GPU-accelerated programs, we formalize the SIMT execution model for a stack-based reconvergence mechanism in an operational semantics and prove its correctness by constructing a simulation between the SIMT semantics and a standard interleaved multi-thread semantics. We also demonstrate that the SIMT execution model produces unfair schedules in some cases. We discuss the problem of unfairness for different batching mechanisms like dynamic warp formation and a stack-less reconvergence strategy.

2011

  • Context-Aware Preference Search for Outdoor Activity Platforms
    W. Kießling, M. Soutschek, A. Huhn, P. Roocks, M. Endres, S. Mandl, F. Wenzel, A. Zelend
    Technical Report, Institute of Computer Science, University of Augsburg, November 2011
    2011-15
  • The Model of Computation of CUDA and its Formal Semantics
    Axel Habermaier
    Technical Report 2011-14, Institute of Computer Science, University of Augsburg
    We formalize the model of computation of modern graphics cards based on the specification of Nvidia’s Compute Unified Device Architecture (CUDA). CUDA programs are executed by thousands of threads concurrently and have access to several different types of memory with unique access patterns and latencies. The underlying hardware uses a single instruction, multiple threads execution model that groups threads into warps. All threads of the same warp execute the program in lockstep. If threads of the same warp execute a data-dependent control flow instruction, control flow might diverge and the different execution paths are executed sequentially. Once all paths complete execution, all threads are executed in parallel again. An operational semantics of a significant subset of CUDA’s memory operations and programming instructions is presented, including shared and non-shared memory operations, atomic operations on shared memory, cached memory access, recursive function calls, control flow instructions, and thread synchronization. Based on this formalization we prove that CUDA’s single instruction, multiple threads execution model is safe: For all threads it is provably true that a thread only executes the instructions it is allowed to execute, that it does not continue execution after processing the last instruction of the program, and that it does not skip any instructions it should have executed. On the other hand, we demonstrate that CUDA’s inability to handle control flow instructions individually for each thread can cause unexpected program behavior in the sense that a liveness property is violated.
  • A Graph Algorithmic Framework for the Assembly of Shredded Documents
    Fabian Richter, Christian X. Ries, Rainer Lienhart
    Technical Report, Institute of Computer Science, University of Augsburg,
    2011-05
  • Swimmer Detection and Pose Estimation for Continuous Stroke Rate Determination
    D. Zecha,T. Greif, R. Lienhart
    Technical Report, Institute of Computer Science, University of Augsburg,
    2011-13
  • Language Modeling with Utterance-Meaning Pairs
    Günther Wirsching, Christian Kölbl
    Technical Report, Institute of Computer Science, University of Augsburg, April 2011
    2011-12
  • Multimodal Ranking for Image Search on Community Databases
    Fabian Richter, Stefan Romberg, Eva Hörster, Rainer Lienhart
    Technical Report, Institute of Computer Science, University of Augsburg,
    2011-07
  • Monocular 3D Human Pose Estimation by Classification
    T. Greif, D. Sengupta, R. Lienhart
    Technical Report, Institute of Computer Science, University of Augsburg,
    2011-09
  • Formal Product Families for Abstract Machines
    A. Zelend
    Technical Report, Institute of Computer Science, University of Augsburg, March 2011
    2011-06

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996