Formal Specs of Database Isolation Done by Chris Newcombe at Amazon for this talk at HPTS 2011 and not used at Amazon. Verified with distributed TLC.