Safety Property: NoThreads

// Don't allow any new threads to be created, or any manipulations of 
// existing threads.

property NoThreads {
  check RSystemThreads.startThread (thread: RThread) {
    violation ("Attempt to start thread.");
  }

  check RSystemThreads.suspendThread (thread: RThread), 
           RSystemThreads.resumeThread (thread: RThread), 
           RSystemThreads.interruptThread (thread: RThread), 
           RSystemThreads.stopThread (thread: RThread), 
           RSystemThreads.destroyThread (thread: RThread) {
    violation ("Thread manipulation attempted.");
  }

  check RSystemThreads.accessGroup (tg: RThread) {
    violation ("Thread group access attempted.");
  }

  check RSystemThreads.createThreadGroup (tg: RThread, name: String) {
    if (name.equals ("main")) {
      ; // We allow the main thread grouop to be created (the system does this).
    } else {
      violation ("Attempt to create thread group: " + name);
    }
  }

  check RSystemThreads.setThreadPriority (thread: RThread, priority: int) {
    violation ("Attempt to set thread priority.");
  }

  check RSystemThreads.setThreadName (thread: RThread, name: String) {
    violation ("Attempt to set thread name: " + name);
  }

  check RSystemThreads.setDaemonThread (thread: RThread),
           RSystemThreads.setUserThread (thread: RThread) {  
    violation ("Attempt to set thread type.");
  }

  check RSystemThreads.setDaemonThreadGroup (tg: RThread), 
           RSystemThreads.setUserThreadGroup (tg: RThread) {
    violation ("Attempt to set thread group type.");
  }

  check RSystemThreads.setMaxPriority (tg: RThread, priority: int) {
    violation ("Attempt to set thread group priority.");
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science