---
title: "Data-Driven Equivalence Checking — Sharma 2013"
description: "Mismatch: the title given is Sharma et al.'s \"Data-Driven Equivalence Checking\", but the supplied text… 22 references, cited by 5 papers here."
authors: ["Rahul Sharma", "Eric Schkufza", "Berkeley Churchill", "Alex Aiken"]
year: 2013
venue: "OOPSLA 2013"
source: "https://theory.stanford.edu/~aiken/publications/papers/oopsla13a.pdf"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/sharma-2013-data-driven-equivalence-checking/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/sharma-2013-data-driven-equivalence-checking/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2013](https://md.research.elamur.ai/free/en/papers/2013/page/2/) / Data-Driven Equivalence Checking

# Data-Driven Equivalence Checking

**Authors:** [Rahul Sharma](https://md.research.elamur.ai/free/en/authors/rahul-sharma/), [Eric Schkufza](https://md.research.elamur.ai/free/en/authors/eric-schkufza/), Berkeley Churchill and [Alex Aiken](https://md.research.elamur.ai/free/en/authors/alex-aiken/) · **Year:** 2013 · **Venue:** OOPSLA 2013 · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1145/2509136.2509509) · [PDF](https://theory.stanford.edu/~aiken/publications/papers/oopsla13a.pdf) · [OpenAlex](https://openalex.org/W2149674423)

**Citations:** 82 citations (OpenAlex, 2026-10-14) · [5](https://md.research.elamur.ai/free/en/papers/sharma-2013-data-driven-equivalence-checking/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
**Mismatch:** the title given is Sharma et al.'s "Data-Driven Equivalence Checking", but the supplied text is a different OOPSLA 2013 paper on Legion by Treichler, Bauer and Aiken. This summary covers the supplied text.

Distributed-memory and GPU machines require data to be split to fit deep memory hierarchies. Earlier systems such as Sequoia and DPJ fix one alias-free partitioning at compile time, which fails when the right split depends on the data. Legion makes logical regions first-class values that can be divided at runtime into subregions, in several ways and possibly overlapping. Tasks declare per-region privileges and coherence modes. The authors formalize Core Legion with a type system and a compositional, asynchronous parallel semantics, and they prove it sound. They also show that if two tasks do not interfere, their subtasks do not either, which justifies a hierarchical, distributed scheduler. Experiments on three real applications confirm that checking pointers statically pays off, while region-level alias checks at runtime are cheap. Dynamic, aliased partitioning is therefore compatible with safety and scalability.

## Key points
- Privileges are read-only, read-write and reduce. Coherence modes are exclusive (the default), atomic and simultaneous.
- Static type checking removes provably safe memory checks, improving performance by up to 71%. Dynamic aliasing checks at region granularity add negligible overhead.
- The Circuit simulation reaches a 62.5X speedup on 96 GPUs of the Keeneland supercomputer, compared with a hand-coded single-GPU version.
- Replacing atomic with exclusive coherence in the Circuit charge-distribution task slows execution by 34% on 48 GPUs and 67% on 96 GPUs, and the penalty grows with node count.
- Compared with Sequoia, DPJ, Chapel, X10, Jade and HPT, Legion uniquely allows multiple dynamic partitions of the same data and per-region coherence.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Stanford University](https://md.research.elamur.ai/free/en/universities/stanford-university/) — University, Stanford, United States · 567 works · 335,189 citations

📚 Shelves (4): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [💻 Software](https://md.research.elamur.ai/free/en/shelves/computer-science/software/) · 150 works

## Cite

Cite as: Rahul Sharma, Eric Schkufza, Berkeley Churchill and Alex Aiken. 2013. Data-Driven Equivalence Checking. OOPSLA 2013.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{sharma2013data,
  title = {{Data-Driven Equivalence Checking}},
  author = {Rahul Sharma, Eric Schkufza, Berkeley Churchill and Alex Aiken},
  booktitle = {OOPSLA 2013},
  year = {2013},
  doi = {10.1145/2509136.2509509},
  url = {https://doi.org/10.1145/2509136.2509509}
}
```

- [← previous Joint Coreference Resolution and Named-Entity Linking with Multi-Pass Sieves](https://md.research.elamur.ai/free/en/papers/hajishirzi-2013-joint-coreference-resolution-named-entity/)
- [next → Multidimensional quality metrics: a flexible system for assessing translation quality](https://md.research.elamur.ai/free/en/papers/lommel-2013-multidimensional-quality-metrics-flexible-system/)
- [↑ back to papers of 2013](https://md.research.elamur.ai/free/en/papers/2013/page/2/)

## References

22 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. M. Bauer, J. Clark, E. Schkufza, and A. Aiken. Programming the memory hierarchy revisited: Supporting irregular parallelism in Sequoia. In Proceedings of the Symposium on Principles and Practice of Parallel Programming, 2011. [find](https://scholar.google.com/scholar?q=M%2E+Bauer%2C+J%2E+Clark%2C+E%2E+Schkufza%2C+and+A%2E+Aiken%2E+Programming+the+memory+hierarchy+revisited%3A+Supporting+irregular+parallelism+in+Sequoia%2E+In+Proceedings+of+the+Symposium+on+Principles+and+Practice+of+Pa)
2. M. Bauer, S. Treichler, E. Slaughter, and A. Aiken. Legion: Expressing locality and independence with logical regions. In Supercomputing (SC), 2012. [find](https://scholar.google.com/scholar?q=M%2E+Bauer%2C+S%2E+Treichler%2C+E%2E+Slaughter%2C+and+A%2E+Aiken%2E+Legion%3A+Expressing+locality+and+independence+with+logical+regions%2E+In+Supercomputing+%28SC%29%2C+2012%2E)
3. C. Bienia. Benchmarking Modern Multiprocessors. PhD thesis, Princeton University, January 2011. [find](https://scholar.google.com/scholar?q=C%2E+Bienia%2E+Benchmarking+Modern+Multiprocessors%2E+PhD+thesis%2C+Princeton+University%2C+January+2011%2E)
4. R. Bocchino et al. A type and effect system for deterministic parallel Java. In OOPSLA, 2009. [find](https://scholar.google.com/scholar?q=R%2E+Bocchino+et+al%2E+A+type+and+effect+system+for+deterministic+parallel+Java%2E+In+OOPSLA%2C+2009%2E)
5. R. Bocchino et al. Safe nondeterminism in a deterministic-by-default parallel language. In POPL, 2011. [find](https://scholar.google.com/scholar?q=R%2E+Bocchino+et+al%2E+Safe+nondeterminism+in+a+deterministic%2Dby%2Ddefault+parallel+language%2E+In+POPL%2C+2011%2E)
6. C. Boyapati, B. Liskov, and L. Shrira. Ownership types for object encapsulation. In POPL, 2003. [find](https://scholar.google.com/scholar?q=C%2E+Boyapati%2C+B%2E+Liskov%2C+and+L%2E+Shrira%2E+Ownership+types+for+object+encapsulation%2E+In+POPL%2C+2003%2E)
7. B.L. Chamberlain et al. Parallel programmability and the chapel language. Int’l Journal of HPC Applications, 2007. [find](https://scholar.google.com/scholar?q=B%2EL%2E+Chamberlain+et+al%2E+Parallel+programmability+and+the+chapel+language%2E+Int%E2%80%99l+Journal+of+HPC+Applications%2C+2007%2E)
8. P. Charles et al. X10: An object-oriented approach to non-uniform cluster computing. In OOPSLA, 2005. [find](https://scholar.google.com/scholar?q=P%2E+Charles+et+al%2E+X10%3A+An+object%2Doriented+approach+to+non%2Duniform+cluster+computing%2E+In+OOPSLA%2C+2005%2E)
9. D. Clarke and S. Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In OOPSLA, 2002. [find](https://scholar.google.com/scholar?q=D%2E+Clarke+and+S%2E+Drossopoulou%2E+Ownership%2C+encapsulation+and+the+disjointness+of+type+and+effect%2E+In+OOPSLA%2C+2002%2E)
10. K. Fatahalian et al. Sequoia: Programming the Memory Hierarchy. In Supercomputing, November 2006. [find](https://scholar.google.com/scholar?q=K%2E+Fatahalian+et+al%2E+Sequoia%3A+Programming+the+Memory+Hierarchy%2E+In+Supercomputing%2C+November+2006%2E)
11. D. Gay and A. Aiken. Language support for regions. In PLDI, 2001. [find](https://scholar.google.com/scholar?q=D%2E+Gay+and+A%2E+Aiken%2E+Language+support+for+regions%2E+In+PLDI%2C+2001%2E)
12. D. Grossman et al. Region-based memory management in cyclone. In PLDI, 2002. [find](https://scholar.google.com/scholar?q=D%2E+Grossman+et+al%2E+Region%2Dbased+memory+management+in+cyclone%2E+In+PLDI%2C+2002%2E)
13. T. Harris, S. Marlow, S. Peyton-Jones, and M. Herlihy. Composable memory transactions. In PPOPP, 2005. [find](https://scholar.google.com/scholar?q=T%2E+Harris%2C+S%2E+Marlow%2C+S%2E+Peyton%2DJones%2C+and+M%2E+Herlihy%2E+Composable+memory+transactions%2E+In+PPOPP%2C+2005%2E)
14. G. Karypis and V. Kumar. A fast and high quality multilevel scheme for partitioning irregular graphs. SIAM J. Sci. Comput., 1998. [find](https://scholar.google.com/scholar?q=G%2E+Karypis+and+V%2E+Kumar%2E+A+fast+and+high+quality+multilevel+scheme+for+partitioning+irregular+graphs%2E+SIAM+J%2E+Sci%2E+Comput%2E%2C+1998%2E)
15. M. Lijewski, A. Nonaka, and J. Bell. Boxlib. [https://ccse.lbl.gov/BoxLib/index.html](https://ccse.lbl.gov/BoxLib/index.html), 2011. [↗](https://ccse.lbl.gov/BoxLib/index.html)
16. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In IEEE Symposium on Logic in CS, 2002. [find](https://scholar.google.com/scholar?q=J%2E+C%2E+Reynolds%2E+Separation+logic%3A+A+logic+for+shared+mutable+data+structures%2E+In+IEEE+Symposium+on+Logic+in+CS%2C+2002%2E)
17. M. C. Rinard and M. S. Lam. The design, implementation, and evaluation of Jade. ACM Trans. Program. Lang. Syst., 1998. [find](https://scholar.google.com/scholar?q=M%2E+C%2E+Rinard+and+M%2E+S%2E+Lam%2E+The+design%2C+implementation%2C+and+evaluation+of+Jade%2E+ACM+Trans%2E+Program%2E+Lang%2E+Syst%2E%2C+1998%2E)
18. M. Tofte and J.P. Talpin. Region-based memory management. In POPL, 1994. [find](https://scholar.google.com/scholar?q=M%2E+Tofte+and+J%2EP%2E+Talpin%2E+Region%2Dbased+memory+management%2E+In+POPL%2C+1994%2E)
19. S. Treichler, M. Bauer, and A. Aiken. Language support for dynamic, hierarchical data partitioning: Extended version. [http://theory.stanford.edu/~aiken/publications/papers/oopsla13a-extended.pdf](http://theory.stanford.edu/~aiken/publications/papers/oopsla13a-extended.pdf), 2013. Technical Report. [↗](http://theory.stanford.edu/~aiken/publications/papers/oopsla13a-extended.pdf)
20. J.S. Vetter et al. Keeneland: Bringing heterogeneous gpu computing to the computational science community. Computing in Science Engineering, pages 90 –95, 2011. [find](https://scholar.google.com/scholar?q=J%2ES%2E+Vetter+et+al%2E+Keeneland%3A+Bringing+heterogeneous+gpu+computing+to+the+computational+science+community%2E+Computing+in+Science+Engineering%2C+pages+90+%E2%80%9395%2C+2011%2E)
21. Y. Yan, J. Zhao, Y. Guo, and V. Sarkar. Hierarchical place trees: A portable abstraction for task parallelism and data movement. In Workshop on Languages and Compilers for Parallel Computing, 2009. [find](https://scholar.google.com/scholar?q=Y%2E+Yan%2C+J%2E+Zhao%2C+Y%2E+Guo%2C+and+V%2E+Sarkar%2E+Hierarchical+place+trees%3A+A+portable+abstraction+for+task+parallelism+and+data+movement%2E+In+Workshop+on+Languages+and+Compilers+for+Parallel+Computing%2C+2009%2E)
22. K. Yelick et al. Titanium: A high-performance Java dialect. In Workshop on Java for High-Performance Network Computing, 1998. [find](https://scholar.google.com/scholar?q=K%2E+Yelick+et+al%2E+Titanium%3A+A+high%2Dperformance+Java+dialect%2E+In+Workshop+on+Java+for+High%2DPerformance+Network+Computing%2C+1998%2E)

*Updated 3 November 2026*