Tuan-Phong Ngo

Tuan-Phong Ngo

Ph.D., Compiler Engineer

CV

also availabe in PDF format

Tuan Phong Ngo

Curriculum Vitae

tuanphong.ngo@gmail.com | https://phongngo.github.io

Education

  • Ph.D in Computer Science, Uppsala University, Sweden, Nov 2013 - Jan 2019
  • M.Sc in Computer Science, Uppsala University, Sweden, Sep 2011 - Jun 2013
    • Average grade: 4.8 (scale from 3 to 5; 3 considered minimum to pass)
    • Selected coursework: Mathematical logic, Artificial intelligence, Advanced algorithms, Advanced computer architecture, Programming theory, Constraint programming, Optimisation, Functional programming, Compiler design, Computer networks, Programming in embedded systems
  • B.Sc and M.Sc in Computer Science, Hanoi University of Science and Technology, Vietnam, Sep 2004 - Jun 2011

Work experience

  • Sep 2020 - now: Compiler Engineer at IAR Systems AB, Uppsala, Sweden
    • Topics: Compiler, Code generation, Assembly code, Optimization, Performance, Code size, Embedded system, C/C++, Agile software development
    • I have been doing research and developing optimization techniques for code generation at both high level and target-dependent level in IAR’s C/C++ compilers. I work closely with generating assembly code for different embedded hardware such as ARM, RISCV, AVR, and Renesas. I gain detailed knowledge in developing high-performance applications from both perspectives of a software developer and a compiler engineer.
    • The job uses C/C++, Visual Studio, Subversion (SVN)/ Git. We also use Agile for software development.
  • Oct 2019 - Sep 2020: C/C++ Developer - Generating Mesh for Rendering Geometric Objects at COMSOL AB at COMSOL AB, Stockhokm, Sweden
    • Topics: Mesh generation, Graphical rendering, High-performance architecture, Cache system
    • COMSOL Multiphysics® is a simulation software for modeling designs used worldwide in research and computer-aided engineering. Mesh, a discretization form of geometry, is used in all COMSOL’s products. The goal of mesh generation is to enable efficient finite-element (FEM) computations based on 3D CAD models and 3D scans.
    • I have designed a new architecture to effectively generate mesh for rendering geometries inside COMSOL Multiphysics®. The new architecture optimizes computation time by 30% on average for large models that contain virtual geometric operations. The core idea of the architecture is using caches of rendering objects at different detail levels for each virtual operation. When a user creates a geometric object by performing a long sequence of operations, a rendering object will be fetched from an appropriate cache for each operation. Then, the rendering object is updated incrementally. Finally, the rendering object is kept for future operations. Because the architecture keeps all necessary rendering information, it does not waste time to redo the same jobs. Therefore, it can obtain a high-performance rendering. It is important to note that I am the main developer implementing almost all mesh generation functions inside the new architecture.
    • The job used C/C++/Java, Visual Studio, and Subversion (SVN).
  • Jun 2019 - Oct 2019: Software verification engineer at IAR Systems Group AB, Uppsala, Sweden
    • Topics: State machine, Software verification, Symbolic model checking, (parallel) BDD
    • Visual State is a product for software design and code generation. I have made several performance improvements for IAR Visual State’s verification engine. Especially, I have developed a new high-performance parallel (multi-core) version of the verification engine.
    • The job used C/C++, Visual Studio, and Subversion (SVN).
  • Mar 2019 - May 2019: Researcher at Department of Information Technology, Uppsala University, Sweden

    • Topics: Software Verification, Stateless model checking, Weak memory models

    • I collaborated with Prof. Bengt Jonsson and Dr. KonstantinosSagonas at the IT department, Uppsala University, to develop a high-performance stateless model checking algorithm for checking the correctness of concurrent programs running under the Sequential consistency semantics.
    • We published a paper “Optimal stateless model checking for reads-from equivalence under sequential consistency” at OOPSLA 2019 - a top conference in Object-oriented programming.
  • Nov 2013 - Jan 2019: Ph.D Student in Computer science at Department of Information Technology, Uppsala University, Sweden
    • Topics: Software model checking, Weak memory models
    • Weak memory model, implemented in modern hardware (e.g., Intel x86-TSO, IBM POWER, or ARM) or modern programming languages (e.g., C/C++11 or Java), obtains high performance by executing instructions in a program out-of-order.
    • This work used formal methods to check the correctness of concurrent programs running under weak memory models. I was the main developer of several efficient tools using C/C++/Python. Publications are in top conferences of software engineering and software verification such as OOPSLA, TACAS, and ESOP.
  • Sep 2013 - Jan 2019: Teaching Assistant at Department of Information Technology, Uppsala University, Sweden
    • I have taken care of lab sessions and home assignments in several courses related to Programming and Program verification such as Programming theory (using Dafny from Microsoft), Data structures and algorithms, Automata and logic in IT system modeling (using SPIN from Bell Lab and CBMC from the University of Oxford).
  • Sep 2009 - Aug 2011: Lecturer at Department of Information Technology, Hanoi University of Science and Technology, Vietnam
    • I gave lectures in several undergraduate courses such as C Programming and Database Design.

Research Interests

  • Compiler optimization
  • Rendering mesh
  • Formal method
  • Software verification
  • Software model checking
  • Weak memory model
  • Data mining

Publications

  • Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. OOPSLA’19.
  • Optimal Stateless Model Checking under the Release-Acquire Semantics. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. OOPSLA’18.
  • Replacing Store Buffers by Load Buffers in TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. VECoS’18.
  • A Load-Buffer Semantics for Total Store Ordering. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. LMCS’18.
  • Context-Bounded Analysis for POWER. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. TACAS’17.
  • The Benefits of Duality in Verifying Concurrent Programs under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. CONCUR’16.
  • Precise and Sound Automatic Fence Insertion Procedure under PSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lång, and Tuan Phong Ngo. NETYS’15.
  • The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan Phong Ngo. ESOP’15.
  • An Efficient Algorithm for Discovering Maximum Length Frequent Itemsets. Tran Anh Tai, Tuan Phong Ngo, and Nguyen Kim Anh. KSE’11.
  • Rule-based Attribute-oriented Induction for Knowledge Discovery. Nguyen Duc Thanh, Tuan Phong Ngo, and Nguyen Kim Anh. KSE’10.
  • Generating Qualified Summarization Answers using Fuzzy Concept Hierarchies. Tuan Phong Ngo, Nguyen Hong Phuong, and Nguyen Kim Anh. SoICT’10.

Grants and Awards

  • Third prize in Artificial Intelligence programming competition, Uppsala University 2019
  • Best-paper award nominee, The European Joint Conferences on Theory and Practice of Software 2017 (ETAPS’17)
  • Best-paper award nominee, The International Conference on Concurrency Theory 2016 (CONCUR’16)
  • Ph.D research grant for period 2013-2018, UPMARC research center
  • Student grant for Summer of code, Google 2012
  • First prize in Functional programming competition, Uppsala University 2012
  • Master scholarship for period 2011-2013, Erasmus Mundus scholarship
  • Vietnamese Government Scholarship for excellent students, Hanoi University of Science and Technology

Talks

Teaching

  • Teaching assistant of Programming theory: Fall 2016, Fall 2017, Fall 2018
  • Teaching assistant of Algorithm and data structures I: Fall 2014, Fall 2015, Fall 2016, Fall 2017, Fall 2018
  • Teaching assistant of Automata and logic in IT system modeling: Fall 2014, Fall 2015, Fall 2016, Fall 2017
  • Lecturer of C programming course: Fall 2009, Fall 2010
  • Lecturer of Database design course: Spring 2009, Spring 2010

Programming Languages and Tools

C/C++ (expert), Java/Python (proficient), SQL (prior experience), Git/Subversion (proficient)

Services

  • Artifact evaluation committee of TACAS’19
  • External reviewer of TACAS’16, TACAS’19
  • External reviewer of VMCAI’16
  • External reviewer of VECoS’18
  • External reviewer of NETYS’15, NETYS’17
  • External reviewer of SoICT’14, SoICT’15, SoICT’16, SoICT’17, SoICT’18

Volunteer

  • Volunteer in ETAPS’17
  • Web master in UPMARC summer school 2018
  • Web master in SoICT’11

References

  • Björn Bretz (Bjorn.Bretz@comsol.com) - Team Leader of Mesh Group, COMSOL AB
  • Prof. Parosh Aziz Abdulla (parosh.abdulla@it.uu.se) - Uppsala University
  • Dr. Mohamed Faouzi Atig (mohamed_faouzi.atig@it.uu.se) - Uppsala University