Towards a Formal Account for Software Transactional Memory