Analyzing stores and references in a parallel symbolic language

We describe an analysis of a parallel language in which processes communicate via first-class mutable shared locations. The sequential core of the language defines a higher-order strict functional language with list data structures. The parallel extensions permit processes and shared locations to be dynamically created; synchronization among processes occurs exclusively via shared locations. The analysis is defined by an abstract interpretation on this language. The interpretation is efficient and useful, facilitating a number of important optimizations related to synchronization, processor/thread mapping, and storage management.