search

arcana-lab / memoir

A case for representing data collections and objects in the LLVM IR
MIT License
12 stars 2 forks source link

Add a MEMOIR Verifier #74

Closed tommymcm closed 2 months ago

tommymcm commented 3 months ago

The Verifier will take a program and check the following conditions are met:

  1. The program is a valid LLVM program (using LLVM's verifier)
  2. All collections in the program maintain linearity (i.e., each collection can be typed linearly)
  3. (optional) The above check can be weakened, and instead check for affine typing, which does not require a collection to be used (this would essentially require that each collection also be deleted)
  4. (optional) For users who want to restrict the program to Gated Single Assignment (GSA) form, an irreducible control flow check can be added.

The goal of this verifier is to make assumptions explicit for passes that deal with destruction of MEMOIR collections.

tommymcm commented 3 months ago

A draft of the Verifier is done.

This relies on memoir/analysis/Liveness.hpp, which relies on NOELLE's Data Flow Analysis.

This issue can be closed once NOELLE is updated to LLVM18 and it has been tested.

tommymcm commented 2 months ago

Tested and pushed to master with bc048dd