Facilities

Gauss Lab          
     
Ganesh Gopalakrishnan   Zvonimir Rakamaric   Mike Kirby  
 
It is an active laboratory for developing new approaches for software verification that target correctness on all levels and abstracton layers of computer systems. Also, it is an active research facility for multiple inter-related and prominent problems in computer sicence, for example: fault-tolerance, reseliency of systems, and automated testing and analysis of HPC and Massively parallel systems.more less
 
SOAR Lab          
         
Zvonimir Rakamaric          
SOAR Lab's research mission is to improve the reliability and resilience of complex software systems by empowering developers with practical tools and techniques for analysis of their artifacts. We are interested in any more technique or method that supports our research mission, including but not limited to: extended static checking, automated theorem proving, model checking, and runtime verification. Currently, our emphasis is on highly automatic and scalable analysis techniques for software, in particular for concurrent software. less
 
CPU Center          
       
Ganesh Gopalakrishnan   Mary Hall      
This is the home of the Center for Parallel computing at Utah (or 'CPU'). CPU will address several critical needs in the growth of our university, including: more
  • channeling the vast array of talent that our university has in the area of parallel computing, and representing this collective strength to external organizations
  • helping advance our capabilities in parallel computing by obtaining external resources and enhancing the placement of our students
  • enriching the talent pool in parallel computing within the university and the Utah region, ultimately leading to the growth of local high-tech jobs
  • enhancing our outreach, including addressing the critical international dimension of the high technology enterprise
  • less
 

Projects

Parachute          
     
Ganesh Gopalakrishnan   Eric Mercer   Vivek Sarkar  
In the Parachute project (“Safely Descend from Static to Dynamic Analysis” — collaboration between Rice University, Brigham Young University and the more University of Utah), the focus is to design dynamic analysis methods that work congruous to the needs of modern high productivity parallel programming languages. We will develop our work around the Rice Habanero Java (HJ) language as a target for our active tester (HAT). The HJ compiler will be modified to generate information for downstream dynamic analysis tools. HJ also has known safe subsets which guarantee various properties. As elaborated in the HJ paper, programming in async language construct for example guarantees deadlock freedom by avoiding waiting/synchronization, while programming in isolated construct guarantees race freedom by enforcing mutual exclusion, and so on. We will modify the HJ compiler to inform the Habanero Active Tester to capitalize on these known subsets and avoid or minimize dynamic checks. The other aspect of HAT is to adjust its operations to match proposed HJ runtimes. HJ runtime has a diverse set of scheduling mechanisms. Some of which are preemptive and some of which are cooperating. Those that are cooperative lead to difficulties in enforcing some behaviors and those that are preemptive may lead to deadlocks and liveness issues. Our tool should be able to explore all of these scenarios and be able to reason about them. The challenges faced for hybrid runtimes verification is that they require both SA and DA but there is still a lot of scope for improving their cooperation. They require rigorous operational semantics specifications. They require simulation of the packaged SA, DA and OpSem (Operational Semantics) to draw conclusions about methodologies effectiveness. More over, HJ has inadequate dynamic verification tools support to aid reason about its programs. HJ has no OpSem specifications, regardless of how heavily they are discussed in published work. This introduces confusions for both tools developers and users of HJ alike. As a result, a concise OpSem is crucially needed to address ambiguity(ies).less
 
FMR Project          
   
Coming soon
 
Ganesh Gopalakrishnan   Zvonimir Rakamaric   Pedro Diniz  
 
Future computing systems are expected to employ tens of billions of transistors, with some recent chips already exceeding the 7 billion mark. The drive for more increased performance per watt and added func- tionality are expected to push future chips to be fabricated in extremely small lithographies. This will increase their propensity to exhibit permanent and transient faults due to noise and radiation. Additional factors—such as the increased usage of dynamic voltage-frequency scaling and power gating—will also increase the frequency of faults. Even without faults occurring, the problem of debugging future large- scale systems will be made difficult by the use of multiple models of concurrency at all levels of system design. The combination of faults and concurrency will exacerbate this situation. Our research focuses on developing: A systematic understanding of how faults can affect the computational and communication behavior of future hardware/software systems Practical methodologies to detect and recover from faults that occur during both sequential and concurrent computations A versatile experimentation infrastructure to validate our solutions. The urgent need for research on resilience enhancement is well documented in the inter-agency workshop report on resilience at extreme scale; a study that identifies challenges that must be overcome before exascale computing systems are realized by year 2020.less
 
URV Project          
     
Ganesh Gopalakrishnan   Martin Berzins   Zvonimir Rakamaric  
The project takes the phisycs simulation platform developed at the University of Utah, a large scale super computing platform, and tries to understand how more it works. The purpose of untderstanding its internals is to instrument it on multiple levels and study and understand how large HPC systems crash and how different faults and bugs manifest. This is a long term project, as well as Uintah itself, and would be the gem stone that integrates all available Formal Verification methods knowledge and innovations we gained or trying to come up with during research. The ultimate goal of this is to develop new more effective approaches to verify large scale parallel and supercomputing systems. In this sense, Uintah will be our real-world lab subject.less
 

Pedagogy

Pedagogy and Educational Projects            
     
Ganesh Gopalakrishnan   Zvonimir Rakamaric   Mike Kirby   Alan Humphrey
 
The academic mission will include a strong emphasis on developing and disseminating new curricular material. There is an acute shortage of information on parallel programming techniques, verification techniques, and performance evaluation/tuning techniques. more We will maintain a prominent web presence where educational resources in these areas will be maintained. It will invite EAB members to visit our campus and offer lectures on advanced topics which will tie into classes on parallelism taught by CPU members and others. less