Muen Make Error (Single CPU)

38 views
Skip to first unread message

Habeeb P

unread,
Nov 6, 2016, 3:28:10 PM11/6/16
to muen-dev
Hi,

I am trying to make Muen for a single CPU system.

The make command output following error (warning).


muen
/kernel/src/sk-mp.adb:51:22: warning: loop range is null, loop will not execute

   compilation of sk
-mp.adb failed

  gprbuild
: *** compilation phase failed
  make
[1]: *** [/home/habeeb/muen5/muen/kernel/obj/debug/kernel] Error 4
  make
[1]: Leaving directory `/home/habeeb/muen5/muen/kernel'
  make: *** [kernel] Error 2


Is it a problem with my compiler or with Muen source code?



kernel/src/sk-mp.adb


procedure Set_Minor_Frame_Barrier_Config
     (Config : Skp.Scheduling.Barrier_Config_Array)
   with
      Refined_Global  => (In_Out => Minor_Frame_Barriers),
      Refined_Depends => (Minor_Frame_Barriers =>+ Config)
   is
   begin
      for I in Config'Range loop
line 52          Barriers.Initialize (Barrier => Minor_Frame_Barriers (I),
                              Size    => SK.Byte (Config (I)));
      end loop;
   end Set_Minor_Frame_Barrier_Config;




Scheduling  element from policy/obj/demo_system_b.xml
<scheduling tickRate="10000">
     <majorFrame>
       <cpu id="0">
<minorFrame barrier="none" subject="tau0" ticks="20"/>
<minorFrame barrier="none" subject="vt" ticks="50"/>
<minorFrame barrier="none" subject="nic_linux" ticks="50"/>
<minorFrame barrier="none" subject="storage_linux" ticks="50"/>
<minorFrame barrier="none" subject="time" ticks="10"/>
<minorFrame barrier="none" subject="dbgserver" ticks="30"/>
</cpu>
<barriers/>
</majorFrame>
</scheduling>



skp-scheduling.ads file contains,  
    
  type Barrier_Index_Range is range 0 .. 0;

   subtype Barrier_Range is
     Barrier_Index_Range range 1 .. Barrier_Index_Range'Last;

 

    type Barrier_Config_Array is array (Barrier_Range) of Barrier_Size_Type;



Here Barrier_Range is 1 .. 0, is it a problem?


Thanking You

Reto Buerki

unread,
Nov 7, 2016, 2:59:15 AM11/7/16
to Habeeb P, muen-dev
Hi,

On 11/06/2016 09:28 PM, Habeeb P wrote:
> I am trying to make Muen for a single CPU system.
>
> The make command output following error (warning).
>
>
> muen/kernel/src/sk-mp.adb:51:22: *warning: loop range is null, loop will
> not execut*e
>
> compilation of sk-mp.adb failed
>
> gprbuild: *** compilation phase failed
> make[1]: *** [/home/habeeb/muen5/muen/kernel/obj/debug/kernel] Error 4
> make[1]: Leaving directory `/home/habeeb/muen5/muen/kernel'
> make: *** [kernel] Error 2
>
>
> *Is it a problem with my compiler or with Muen source code?*

Your compiler is fine, this is a known problem. We have not tackled it
because all our existing configurations utilize multiple physical CPU cores.

Assuming that your target platform provides multiple physical cores,
what is your use case? Is it a requirement that only one core is used?

Kind regards
- reto

Habeeb P

unread,
Nov 19, 2016, 2:28:18 AM11/19/16
to muen-dev
Hi

Thanks for the reply.

We are trying to verify the muen separation kernel.
we would like to start with a simpler (single CPU) system.
Is it possible to modify the code to work in single CPU system?
If you have such a code please share with us.


Thanking you
HABEEB P

Reto Buerki

unread,
Nov 21, 2016, 4:46:15 AM11/21/16
to Habeeb P, muen-dev
Hi,

On 11/19/2016 08:28 AM, Habeeb P wrote:
> We are trying to verify the muen separation kernel.

That is interesting. As we are planning to verify functional properties
of the kernel ourselves, it might make sense to coordinate our efforts.

Could you outline what you are planning to verify? If it is not ready
for public discussion, don't hesitate to contact me privately.

> we would like to start with a simpler (single CPU) system.
> Is it possible to modify the code to work in single CPU system?
> If you have such a code please share with us.

We will look into it.

Kind regards,
- reto
Reply all
Reply to author
Forward
0 new messages