Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add SC-per-Location Axiom #6

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Add SC-per-Location Axiom #6

wants to merge 1 commit into from

Commits on May 21, 2023

  1. Add SC-per-Location Axiom 

    This commit adds the Sequential Consistency Per Location axiom(https://docs.nvidia.com/cuda/parallel-thread-execution/index.html#sc-per-loc-axiom) which is missing in the model. We add a litmus test from issue(NVlabs#4). If the Program Order (PO) relation removed from cause_base relation which makes the model roll back to ptx-v6.0 (proxy-less version), this test shows the SC-per-Location axiom is missing.

Co-authored-by: Hernan Ponce de Leon <[email protected]>
    @tonghaining @hernan-poncedeleon
    tonghaining and hernan-poncedeleon committed May 21, 2023
    Configuration menu
    Copy the full SHA
    ad03ba3 View commit details
    Browse the repository at this point in the history