1/* 2 * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7import <std_connector.camkes>; 8 9import "components/Client/Client.camkes"; 10import "components/Server/Server.camkes"; 11 12assembly { 13 composition { 14 component Client client_1; 15 component Client client_2; 16 component Server server; 17 18 connection seL4RPCCall client_1_server(from client_1.i, from client_2.i, to server.i); 19 } 20 configuration { 21 client_1._priority = 50; 22 client_2._priority = 50; 23 server.i_priority = 60; 24 25 /* The following parameters only have an effect on 26 the MCS kernel */ 27 client_1._period = 10000; 28 client_1._budget = 10000; 29 client_2._period = 10000; 30 client_2._budget = 10000; 31 server.i_period = 10000; 32 server.i_budget = 10000; 33 // server.i_passive = true; 34 } 35} 36 37/* 38Scenarios to consider: 39- priority: 40 - client priority == server priority - succeed 41 - client priority < server priority - succeed 42 - client priority > server priority - succeed 43- scheduling context 44 - client has enough SC: succeed 45 - client doesn't have enough SC: succeed (roll over to the next period) 46 - server has enough SC: succeed 47 - server doesn't have enough SC: succeed (roll over to the next period) 48- if client/server doesn't have enough SC 49 - budget << period: succeed - longer delay 50 - budget < period: succeed - shorter delay 51 - budget = period: succeed - no delay 52 53should we time how long the calls take? or does it matter (thinking behind this: tell the difference between a call succedding in one period or having to wait for it to reset and continuing when it goes over budget and also how long the period is) 54 55*/ 56