skip to main content

Search for: All records

Creators/Authors contains: "Wu, Wenhao"

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Enea, Constantin ; Lal, Akash (Ed.)
    Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP. 
    more » « less
    Free, publicly-accessible full text available July 18, 2024
  2. Preaxial dominance in the mesopodium is limited to distal carpals/tarsals and facilitates digit reduction in early tetrapods. 
    more » « less
  3. Fisman, Dana ; Rosu, Grigore (Ed.)
    Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran's unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application. 
    more » « less
  4. In many packet-switched wireless systems including cellular networks, RObust Header Compression (ROHC) plays an important role in improving payload efficiency by reducing the number of header bits in a link session. However, there are only very few research works addressing the optimized control of ROHC. Our recent studies have demonstrated the advantage of a trans-layer ROHC design that exploits lower layer link status. We have presented a unidirectional ROHC design based on a partially observable Markov decision process formulation that enables the transmitter to decide the header compression level without receiver feedback. The present work considers the physical channel dynamics in an LTE environment and how they affect header decompressor status. Our new model takes into consideration the transport block (TBs) size defined in LTE transmission according to the modulation and coding scheme (MCS). Our novel and practical model can significantly improve the efficiency of the transmission when compared to a traditional timer-based ROHC control. 
    more » « less