PSO Reachability and Fence Insertion

I have added an abstraction of the PSO memory model and implemented sound and complete reachability analysis for finite data domains.