In this question, you will formalize requirements about yet another high$-$performance computing centre.

The high$-$performance computing centre consists of a group of CPUs. Different CPUs may have different amounts

of memory and provide different levels of security.

Each program has a minimum security level and a minimum amount of memory that it needs to run on a CPU.

Allocation is the process of assigning programs to the CPU that they will run on$.$ An allocation is a set of

$($prog$,$ cpu$)$ pairs indicating which CPU each program will run on$.$

Given the environment:

Type cpu $//$ CPUs

Type prog $//$ programs

Type mem :$=$ N $//$ amount of memory

Type seclvl :$=$ N $//$ security level

Type alloc :$=$ set$(($prog$,$ cpu$))//$ allocation

to mem$($c : cpu$)$ : N $//$ the total amount of memory on the CPU

to mem$($p : prog$)$ : N $//$ the memory required by the program

to sec$($c : cpu$)$ : seclvl $//$ the security level provided by the CPU

to sec$($p : prog$)$ : seclvl $//$ the security level required by the program

Notes:

$1.$ The functions to mem and to sec are overloaded to work on both CPUs and programs.

$2.$ All programs are unique. You do not need to worry about supporting two copies of the same program.

$3.$ All CPUs are unique.

Q$2$a Formalization $(8$ marks$)$

$1.$ Formalize the requirement below as a predicate mem ok that takes an allocation as an argument and deter$-$

mines whether the allocation satisfies the requirement.

Requirement: The total amount of memory required by all of the programs allocated in A to any CPU is

less than the total amount of memory on the CPU.

$2.$ Formalize the requirement below as a predicate is optimal that takes an allocation as an argument and deter$-$

mines whether the allocation satisfies the requirement.

The formalization of is optimal may use functions that you defined as part of the first requirement.

Requirement: For any program allocated in A to any CPU, there is not another CPU with a lower security

level that could be allocated to the program, where $$could be allocated$$ means that CPU$$s security level is at

least as high as that required by the program and the CPU has sufficient unused memory for the program to

run.

Q$2$b Code review $(4$ marks$)$

The two functions below, addalloc$1$ and addalloc$2$ are intended to allocate a program to a CPU and satisfy the

requirements above.

Your task is to determine if each function behaves as intended.

Notes:

$1.$ Assume that there is at least one CPU in A that could be allocated to p$.$ That is$,$ you do not have to worry

about errors or failures in allocation.

$2.$ Assume that all values of type cpu are in A$.$

$3.$ If a function does not behave as intended, describe the unintended behaviour and explain why the code causes

the function to have the behaviour you describe. $($e$.$g$.,$the function always returns the empty set, because it

tests if CompEng students have a life in the real world, which is always false.$)$

$4.$ If a function behaves as intended, give a brief brief informal justification.

add alloc$1($p$1$ : prog, A : alloc$)$ : alloc :$=$

val A$$ : alloc $=\{($p$2,$ c$2)|$ p$2$ in to progs$($A$)\backslash$cup $\{$p$1\},$ c$2$ in to cpus$($A$)\}$

$\{($p$3,$ c$3)|($p$3,$ c$3)$ in A$.($p$3,$ c$3)$ in A $$ could alloc$($p$3,$ c$3,$ A$)$ is optimal$($A$)\}$

add alloc$2($p$1$ : prog, A : alloc$)$ : alloc :$=\{($p$2,$ c$2)|$ p$2$ : prog, c$2$ : cpu $.($p$2,$ c$2)$ in A $($mem ok$($A $\backslash$cup $\{($p$2,$ c$2)\})$ is optimal$($A $\backslash$cup $\{($p$2,$ c$2)\})($p$1=$ p$2)$