Stateless model checking concurrent programs with maximal causality reduction