title: Any systematic way to avoid "reentry" problem? (embedded system)
body: <p>We are using C to build a system on ARM core (i.e. an embedded system). The question is: how can we avoid reentry problem in a formal way so that we are confident all reentry bugs are removed. This may not be a practical wish but surely important for any system, I guess.</p>
  
  <p>Just for the discussion, I guess drawing UML diagram or have a complete state machine would be a good start (but how to generate it AFTER the whole system is developed?). Any suggestions on how to use state machine / UML diagram to do the analysis?</p>