Safety Property: SafeThreads



property SafeThreads {    
    requires TrackThreadsTrackThreadGroupsStoreThread;

    helper checkThreadAccess (thread: RThread) {
        if (naccio.library.NCheck.isInitialized ()) {
            SecurityManager security = getSecurityManager ();
            if (security != null) {    
                security.checkAccess (thread.getThread ());
            }   
        }
    }
  
    helper checkThreadGroupAccess (tg: RThread) {
        if (naccio.library.NCheck.isInitialized ()) {
            SecurityManager security = getSecurityManager ();
            if (security != null) {    
                security.checkAccess (tg.getThreadGroup ());
            }   
        }
    }
  
    check RSystemThreads.accessGroup (tg: RThread) {
        checkThreadGroupAccess (tg);
    }
  
    check RSystemThreads.createThreadGroup (tg: RThread, name: String) {
        checkThreadGroupAccess (tg);
    }
  
    check RSystemThreads.setThreadPriority (thread: RThread, priority: int) {
        checkThreadAccess (thread);
    }     

    check RSystemThreads.setMaxPriority (tg: RThread, priority: int) {
        checkThreadGroupAccess (tg);
    }     

    check RSystemThreads.setThreadName (thread: RThread, name: String) {
        checkThreadAccess (thread);
    }

  
    check RSystemThreads.startThread (thread: RThread),
          RSystemThreads.suspendThread (thread: RThread),
          RSystemThreads.resumeThread (thread: RThread),
          RSystemThreads.interruptThread (thread: RThread),
          RSystemThreads.stopThread (thread: RThread),
          RSystemThreads.destroyThread (thread: RThread) {
        checkThreadAccess (thread);
    }
    
    check RSystemThreads.setDaemonThread (thread: RThread),
          RSystemThreads.setUserThread (thread: RThread) {
        checkThreadAccess (thread);
    }     

    check RSystemThreads.setDaemonThreadGroup (tg: RThread),
          RSystemThreads.setUserThreadGroup (tg: RThread) {
        checkThreadGroupAccess (tg);
    }     

    check RSystemThreads.getGroupParent (tg: RThread) {
        checkThreadGroupAccess (tg);
    }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science