3. RELEVANT TEORI
3.1 B EGREPSAVKLARING
Para tratar dos requisitos do FreeRTOS ligados à prioridade de uma tarefa, é necessário inicialmente acrescentar tal característica à modelagem. Esse acréscimo está relacionado principalmente à máquina Task, onde o elemento tarefa é especificado, e pode ser feito de duas formas: escrevendo uma nova versão para essa máquina ou refinando-a. Aqui, a última forma foi escolhida como a mais adequada.
O refinamento da máquina Task é feito pelo módulo Task_priority. Neste, um novo estado é declarado adicionando a característica de prioridade de uma tarefa e, em seguida, suas operações são refeitas para tratar essas características. O estado desse refinamento e suas operações serão explicados nas seções a seguir.
7.1.1 Estado do Task_priority
O estado do refinamento Task_priority pode ser visto na figura 7.1. Nele são criados duas novas variáveis responsáveis por associar uma tarefa a uma prioridade, t_priority e t_bpriority. A primeira informa a prioridade atual da tarefa e a segunda informa a prioridade real da tarefa. Essas duas prioridades foram criadas devido ao mecanismo de herança de prioridade, onde uma tarefa herda momentaneamente a prioridade de outra. Assim, quando uma tarefa herda a prioridade de outra, a sua prioridade real é armazenada em t_bpriority e a sua prioridade atual é alterada.
Junto com o estado da figura 7.1 foi criada a função schedule_p para ajudar na es- pecificação das propriedades relacionadas à prioridade de uma tarefa. Essa função tem como objetivo escolher, baseado na política de prioridade do escalonador, um conjunto de tarefas que podem entrar em execução. Assim, ela tem como entradas o conjunto de
tarefas prontas (onde será realizada a seleção) e as prioridades das tarefas (para as regras da seleção). Desse modo, a função seleciona as tarefas com maior prioridade no conjunto de tarefas prontas e retorna um conjunto formado pelas tarefas selecionadas.
REFINEMENT Task_priority CONSTANTS
max_prt, schedule_p PROPERTIES
schedule_p ∈ (FIN(TASK ) ∗ (TASK →+ PRIORITY )) →+ FIN(TASK )∧
schedule_p = ∀(tasks, t_priority).(tasks ∈ FIN(TASK )∧
t_priority ∈ TASK →+ PRIORITY ∧
tasks�= ∅ ∧ tasks ⊂ dom(t_priority)
|tasks ∩ dom(t_priority �{max(t_priority[tasks])})) VARIABLES
t_priority t_bpriority INVARIANT
t_priority ∈ TASK →+ PRIORITY ∧
dom(t_priority) = tasks ∧
t_bpriority ∈ TASK →+ PRIORITY ∧
dom(t_bpriority) = tasks ∧ (active = TRUE ⇒
t_priority(idle) = IDLE _PRIORITY ∧
t_priority(running) = max(t_priority[runnable])∧ IDLE_PRIORITY ≤ min(t_priority[tasks]))
Figura 7.1: Estado Task_priority.
Por último, nas três linhas finais do estado da figura 7.1, foram colocadas restrições relacionadas à prioridade de tarefas especiais. A primeira delas informa que a tarefa ociosa terá prioridade ao parâmetro de configuração do sistema IDLE _PRIORITY . A segunda especifica que a tarefa em execução deve ser a tarefa de maior prioridade do conjunto de tarefas aptas para entrar em execução. Por último, tem-se que a prioridade da tarefa ociosa deve ser menor que as demais.
7.1.2 Operações
As operações da máquina Task_priority são refinamentos das operações da máquina Task. Devido a isso, Task_priority possui as mesmas operações de Task, mas especifi- cadas de forma diferentes. Entretanto, no capítulo anterior, algumas operações de Task, relacionadas principalmente à prioridade de uma tarefa, não foram comentadas, sendo estas explicadas somente nesta seção.
As operações que tratam somente da prioridade de uma tarefa são: t_getPriority, t_setPriority. A primeira operação é bastante simples, apenas retorna a prioridade de uma tarefa utilizando a asserção priority := t_priority(atask), onde priority é o parâmetro de retorno da operação e atask é a tarefa que será retornada a prioridade. Na segunda, a prioridade da tarefa é alterada. Essa operação possui um funcionamento um pouco mais complexo e será comentada na seção 7.1.2.4.
Entre as demais operações refinadas dá máquina Task, uma das principais alter- ações nas suas especificações ocorreu na escolha da tarefa em execução, que anteri- ormente era feita através de uma atribuição indeterminada sobre o conjunto runnable,
running :∈ runnable. Com o refinamento, essa escolha passou a ser mais precisa, feita em cima do conjunto retornado pela função schedule_p, semelhante à asserção running :∈ schedule_p(n_runnable, n_priority), que será melhor explicada nas seções seguintes através do refinamento das operações t_create, t_resume, t_priorityInherit e t_setPriority.
7.1.2.1 Operação t _create
O refinamento da operação t_create difere da sua operação abstrata da figura 6.5 pelo fato de que a nova tarefa criada deve possuir também uma prioridade base e uma prioridade atual, especificadas pelas variáveis t_bpriority e t_priority, respectivamente. Assim, como demonstra a figura 7.2, na criação de uma nova tarefa através da substituição ANY, a prioridade passada como argumento é associada a ela. Essa associação ocorre tanto na prioridade base como na prioridade atual. Uma melhor explicação desses dois tipos de prioridade será vista especificação da operação t_priorityInherit na seção 7.4.
result←− t_create(priority) = BEGIN ANY task , n_runnable, n_priority WHERE task ∈ TASK ∧ task �∈ tasks∧ n_runnable ⊂ tasks∧
n_runnable = runnable ∪ {task}∧
task �= TASK _NULL∧
n_priority ∈ TASK →+ PRIORITY ∧
n_priority =
t_priority ∪ {task �→ priority} THEN
tasks:= tasks ∪ {task } �
runnable := n_runnable �
t_priority := n_priority � t_bpriority :=
t_bpriority ∪ {task �→ priority} �
IFactive= TRUE THEN
IFpriority ≤ t_priority(running) THEN
running:∈
schedule_p(n_runnable, n_priority) END ELSE IFrunnable = ∅ THEN running:= task ELSE IFpriority ≥ t_priority(running) THEN running :∈
schedule_p(n_runnable, n_priority) END END END� result:= task END END;
Figura 7.2: Refinamento da operação t_create.
Outro detalhe sobre a operação da figura 7.2 pode ser visto no momento da escolha da tarefa em execução. Pois, nessa operação, é verificado se a prioridade da tarefa a ser criada é maior que a tarefa em execução. Como o escalonador deve manter a tarefa pronta de maior prioridade em execução, caso a prioridade da nova tarefa seja maior que a da tarefa em execução, uma nova escolha é feita pela asserção running :∈ schedule_p(n_runnable, n_priority).
7.1.2.2 Operação t _resume
No refinamento da operação t_resume da figura 7.3 as alterações geradas para tratar a prioridade de uma tarefa foram: verificar se é necessário realizar uma nova escolha da tarefa em execução e realizar de forma mais determinística essa escolha. Assim, no início
da operação, a tarefa que deve ser retornada é colocada no estado pronta e, em seguida, é verificada se sua prioridade é maior ou igual que a da tarefa em execução. Caso essa verificação seja verdadeira, uma nova escolha da tarefa em execução é realizada.
t_resume(rtask) = BEGIN ANY n_runnable WHERE n_runnable ⊂ tasks∧
n_runnable = runnable ∪ {rtask} THEN
runnable := n_runnable �
IFt_priority(rtask) ≥ t_priority(running) THEN
running :∈ schedule_p(n_runnable, t_priority) END
END�
suspended := suspended − {rtask }
END;
Figura 7.3: Refinamento da operação t_create.
7.1.2.3 Operação t _priorityInherit
A operação t_priorityInherit preocupa-se com o mecanismo de herança de priori- dade do mutex. Desse modo, esse refinamento manipula principalmente os campos de prioridade base e prioridade atual da tarefa que mantém o mutex, como demonstra a figura 7.4. Para realizar a herança de prioridade, a tarefa que mantém o mutex é pas- sada através do parâmetro holderTask. Após isso, a prioridade atual dessa tarefa é substituída pela prioridade da tarefa em execução através das asserções n_priority = t_priority <+{holderTask �→ t_priority(running)} e t_priority := n_priority. Vale lembrar que, a prioridade real da tarefa que mantém, o mutex está em t_bpriority. Assim, quando o mutex for liberado, a prioridade atual da tarefa que mantém o mutex retorna para sua prioridade original. Essa ação é feita pela operação t_returnPriority.
7.1.2.4 Operação t _setPriority
Por fim, a operação t_setPriority é responsável por alterar a prioridade de uma tarefa. Para isso, a prioridade e a tarefa a serem alteradas devem ser passadas como parâmetro, conforme a figura 7.5. Após essas informações, a prioridade da tarefa é alterada pelas substituições n_priority := t_priority <+{task �→ priority}, t_priority := n_priority e t_bpriority(task) := priority. Percebe-se, nesse momento, que tanto a prioridade atual da tarefa como a sua prioridade base são alteradas.
No final da especificação da figura 7.5, ao alterar a prioridade de uma tarefa, é verifi- cado se a nova prioridade é maior ou igual à prioridade da tarefa em execução. Caso essa afirmação seja verdadeira, será necessário realizar a escolha de uma nova tarefa para en- trar em execução (running :∈ schedule_p(runnable, n_priority)). Caso negativo, nada é realizado.
t_priorityInherit(holderTask, xTicksToWait) = BEGIN ANY n_runnable, npriority WHERE n_runnable ⊂ tasks∧
n_runnable = runnable − {running}∧ n_runnable �= ∅∧
n_priority ∈ TASK →+ PRIORITY ∧
n_priority = t_priority <+{holderTask �→ t_priority(running)} THEN
runnable := n_runnable �
blocked := blocked ∪ {running} �
IFt_priority(running) > t_priority(holderTask) THEN t_priority := n_priority �
t_bpriority(holderTask) := t_priority(holderTask) � running:∈ schedule_p(n_runnable, n_priority) ELSE
running:∈ schedule_p(n_runnable, t_priority) END
END END;
Figura 7.4: Refinamento da operação t_priorityInherit.
t_setPriority(task, priority) = BEGIN
ANY n_priority WHERE
n_priority = t_priority <+{task �→ priority} THEN
t_priority := n_priority � t_bpriority(task) := priority �
IFtask∈ runnable THEN
IFt_priority(running) ≤ priority THEN
IFtask�= running THEN
running:∈ schedule_p(runnable, n_priority) END
ELSE
IFtask= running THEN
running:∈ schedule_p(runnable, n_priority) END
END END END END;
Figura 7.5: Refinamento da operação t_setPriority.