JRF-E: using model checking to give advice on eliminating memory model-related bugs.