Whether a mutual exclusion protocol is correct, in the sense that it satisfies starvation freedom besides mutual exclusion, depends on the fairness assumption one makes (or completeness criterion one imposes). A rough classification of completeness criteria (in increasing strength) is
None -- Progress -- Justness -- Weak fairness -- Strong Fairness -- Full fairness
When making no fairness assumption, correct mutual exclusion is impossible. When assuming weak fairness, classical algorithms, like Peterson's or Lamport's bakery, work correctly. But (weak) fairness is an assumption that is typically unwarranted, unlike progress or justness, which can be safely assumed. Whether mutual exclusion is possible at all, when merely assuming justness, depends on our hardware, and on whether we want our protocol to be speed independent. When assuming "atomicity", implying that a first memory access needs to be completed before a second one can start, no speed independent mutual exclusion is possible at all (without assuming fairness). But if we give up up speed independence or atomicity it is, and I can show how to model this in process algebra.