Wiki

資源管理

資源管理に係る観測と遷移

OSEK/VDX仕様では陽に触れられていないが，後にシステムサービスを記述する際に必要になる２つの遷移，資源の占有と解放をCafeOBJで記述する．この２つの遷移を記述するには，処理単位が占有している資源の集合，および，資源を占有している処理単位の集合を返す観測を宣言しておかなければならない．

まず，資源を項に持つソートを宣言する．

#!python

module RESOURCE
{
  signature
  {
    [ Resource ]
  }
}

資源には，外部資源と内部資源の２種類があった．

#!python

module EXTERNAL-RESOURCE
{
  imports
  {
    ex(RESOURCE)
  }
  signature
  {
    [ ExternalResource < Resource ]
  }
}

#!python

module INTERNAL-RESOURCE
{
  imports
  {
    ex(RESOURCE)
  }
  signature
  {
    [ InternalResource < Resource ]
  }
}

外部資源はソートExternalResourceの項として，内部資源はソートInternalResourceの項として表現される．

資源，外部資源，および，内部資源の集合を表すモジュールを各々次のように宣言する．

#!python

make RESOURCES
(
  SET(RESOURCE{sort Elt -> Resource})*{sort Set -> Resources}
)

#!python

make EXTERNAL-RESOURCES
(
  SET(EXTERNAL-RESOURCE{sort Elt -> ExternalResource})*{sort Set -> ExternalResources}
)

#!python

make INTERNAL-RESOURCES
(
  SET(INTERNAL-RESOURCE{sort Elt -> InternalResource})*{sort Set -> InternalResources}
)

次に，上で宣言した資源の集合を観測結果として返す観測を次のように宣言する．

#!python

module OBSERVATION2RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    ex(RESOURCES)
  }
  signature
  {
    [ Observation2Resources < Observation ]
    [ Resources < Value ]
    op __ : Observation2Resources Container -> Resources
  }
}

#!python

module OBSERVATION2EXTERNAL-RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    ex(EXTERNAL-RESOURCES)
  }
  signature
  {
    [ Observation2ExternalResources < Observation ]
    [ ExternalResources < Value ]
    op __ : Observation2ExternalResources Container -> ExternalResources
  }
}

#!python

module OBSERVATION2INTERNAL-RESOURCES
{
  imports
  {
    ex(OBSERVATION)
    ex(INTERNAL-RESOURCES)
  }
  signature
  {
    [ Observation2InternalResources < Observation ]
    [ InternalResources < Value ]
    op __ : Observation2InternalResources Container -> InternalResources
  }
}

上のモジュールを輸入して，処理単位が占有している資源の集合を返す観測を定める．

#!python

module OCCUPYING
{
  imports
  {
    ex(OBSERVATION2RESOURCES)
    pr(ENTITY)
    pr(STATE)
  }
  signature
  {
    op occupying : Entity -> Observation2Resources
  }
  axioms
  {
    vars X : Entity
    eq occupying(X)(init) = nil .
  }
}

初期状態においては，どの処理単位も資源を占有していない．

資源が占有されている処理単位の集合を返す観測は次のようにして定められる．

#!python

module OCCUPIED
{
  imports
  {
    ex(OBSERVATION2ENTITIES)
    pr(RESOURCE)
    pr(STATE)
  }
  signature
  {
    op occupied : Resource -> Observation2Entities
  }
  axioms
  {
    vars R : Resource
    eq occupied(R)(init) = nil .
  }
}

初期状態では，資源はどの処理単位にも占有されていない．

この２つの観測を用いて，資源の占有と解放を表すモジュールを記述しよう．どの処理単位がどの資源を占有するかがが予め明らかになっているものとする．

#!python

module ACCESS
{
  imports
  {
    pr(RESOURCE)
    pr(ENTITY)
  }
  signature
  {
    op access : Entity Resource -> Bool
  }
}

資源を占有する遷移と開放する遷移を，各々OCCUPYとFREEというモジュールで定める．処理単位は，予め占有すると明らかになっている資源しか実際に占有できない．具体的には，処理単位xが資源rを占有する場合には，access(x,r)が真でなければならない．また，処理単位は，既に占有されている資源を占有することはできない．

#!python

module OCCUPY
{
  imports
  {
    ex(STATEMACHINE)
    pr(OCCUPYING)
    pr(OCCUPIED)
    pr(ACCESS)
  }
  signature
  {
    [ Occupy < Transition ]
    op sub : Occupy -> Entity
    op res : Occupy -> Resource
  }
  axioms
  {
    vars C : State
    vars T : Occupy
    cq access(sub(T),res(T)) = true
       if pre(T,C) .
    cq occupied(res(T))(C) = nil
       if pre(T,C) .
    cq occupying(sub(T))(T(C)) = (occupying(sub(T))(C)),res(T)
       if pre(T,C) .
    cq occupied(res(T))(T(C)) = (occupied(res(T))(C)),sub(T)
       if pre(T,C) .
    eq rev(T,occupying(sub(T))) = true .  
    eq rev(T,occupied(res(T))) = true .  
  }
}

資源を解放する際には，その資源は解放する処理単位に占有されていなければならない．

#!python

module FREE
{
  imports
  {
    ex(STATEMACHINE)
    pr(OCCUPYING)
    pr(OCCUPIED)
  }
  signature
  {
    [ Free < Transition ]
    op sub : Free -> Entity
    op res : Free -> Resource
  }
  axioms
  {
    vars C : State
    vars T : Free
    cq sub(T) @ occupied(res(T))(C) = true
       if pre(T,C) .
    cq occupying(sub(T))(T(C)) = (occupying(sub(T))(C)) \ res(T)
       if pre(T,C) .
    cq occupied(res(T))(T(C)) = (occupied(res(T))(C)) \ sub(T)
       if pre(T,C) .
    eq rev(T,occupying(sub(T))) = true .  
    eq rev(T,occupied(res(T))) = true .  
  }
}

処理非活性化時の制約

タスクがその処理を終了する際には，占有した資源を全て解放しておかなければならない．このことは，次のように表される．

#!python

module OCCUPATION-on-DISABLE
{
  imports
  {
    pr(DISABLE)
    pr(OCCUPYING)
    pr(EXTERNAL-RESOURCE)
  }
  axioms
  {
    vars C : State
    vars T : Disable
    vars R : ExternalResource
    cq R @ occupying(sub(T))(C) = false
       if pre(T,C) .
  }
}

後で触れる内部資源を考慮して，ここでは，非活性化前には占有した外部資源は全て解放されていること，という条件を記述している．

資源としてのスケジューラ

スケジューラは，外部資源とも見なされる．このことは，次のようなCafeOBJモジュールで表現できる． OSEK OS では，RES_SCHEDULERという予め決められた名前のリソースが生成される．

#!python

module SCHEDULER
{
  imports
  {
    ex(INTERNAL-ACTIVITY)
    ex(RESOURCE)
  }
  signature
  {
    [ Scheduler < InternalActivity Resource ]
    op RES-SCHEDULER : -> Scheduler
  }
}

内部資源

内部資源を占有できるのはタスクに限られる．内部資源はユーザからは見えないので，システムサービスを通して占有・解放することはできない．その代わり，システム生成時に内部資源を高々１つタスクに割り当てることができる．タスクに割り当てられた内部資源は，実行開始の際にそのタスクに占有される．そして，遷移preemptでは開放されないが，タスクの終了やタスクからのスケジューラ呼出時には自動的に解放される．まず，システム生成時にタスクに割り当てられている内部資源を次のモジュールで宣言する．

#!python

module ASSOCIATE
{
  imports
  {
    pr(TASK)
    pr(INTERNAL-RESOURCES)
    pr(ACCESS)
  }
  signature
  {
    op associate : Task -> InternalResources
  }
  axioms
  {
    vars X : Task
    vars R : InternalResource
    eq #(associate(X)) <= 1 = true .
    cq access(X,R) = true
       if R @ associate(X) .
  }
}

実行開始時に内部資源が実行タスクに占有されることを記述するには，そのタスクがこれまでに実行されたことがあるか否かを表す観測が必要になる．

#!python

module EXECUTED
{
  imports
  {
    ex(OBSERVATION2BOOL)
    pr(TASK)
  }
  signature
  {
    op executed : Task -> Observation2Bool
  }
}

実行開始を表すSTARTを次のように書き換える．

#!python

module START
{
  imports
  {
    ex(RUN)
    ex(EXIT)
    pr(ASSOCIATE)
    pr(OCCUPYING)
    pr(OCCUPIED)
    pr(EXECUTED)
  }
  signature
  {
    [ Start < Run Exit ]
    op start : Task -> Start
    op sub : Start -> Task
  }
  axioms
  {
    vars C : State
    vars X : Task
    vars T : Start
    vars R : InternalResource
    eq sub(start(X)) = X .
    cq occupying(sub(T))(T(C)) = associate(sub(T))
       if pre(T,C) and not(executed(sub(T))(C)) .
    cq occupied(R)(T(C)) = (sub(T), occupied(R)(C))
       if pre(T,C) and R @ associate(sub(T)) .
    cq executed(sub(T))(T(C)) = true
       if pre(T,C) .
    cq rev(T,occupying(sub(T))) = true
       if not(executed(sub(T))(C)) .
    cq rev(T,occupied(R)) = true
       if R @ associate(sub(T)) .
    eq rev(T,executed(sub(T))) = true .
  }
}

実行されるタスクがまだ実行されたことがなければ，タスクは自身に割り当てられている内部資源を占有し，内部資源の占有者には実行されるタスクが追加される．

#!python

module TERMINATE
{
  imports
  {
    ex(DISABLE)
    ex(STOP)
    pr(SUSPENDED)
    pr(OCCUPYING)
    pr(OCCUPIED)
    pr(INTERNAL-RESOURCE)
  }
  signature
  {
    [ Terminate < Stop Disable ]
    op terminate : Task -> Terminate
    op sub : Terminate -> Task
  }
  axioms
  {
    vars C : State
    vars X : Task
    vars T : Terminate
    vars R : InternalResource
    eq sub(terminate(X)) = X .
    cq suspended(T(C)) = (suspended(C)),X
       if pre(T,C) .
    cq occupying(sub(T))(T(C)) = nil
       if pre(T,C) .
    cq occupied(R)(T(C)) = occupied(R)(C) \ sub(T)
       if pre(T,C) and R @ occupying(sub(T))(C) .
    eq rev(T,suspended) = true .
    eq rev(T,occupying(sub(T))) = true .
    cq rev(T,occupied(R)) = true
       if R @ occupying(sub(T))(C) .
  }
}

タスクの終了に伴い内部資源は全て解放され，終了したタスクは，内部資源の占有者から外される．