EE249 Course Project Timing Based Communication Refinement for CFSMs Presenters Mentors Professor Heloise Hse Irene Po Jonathan Martin Marco Sgroi Alberto Sangiovanni Vincentelli Outline Problem descriptions Rendezvous based communication Buffer sizing Mixed HW SW implementation with CPU contention Unresolved Issues Conclusion Problem Descriptions Currently CFSM networks in Polis use oneplace buffer Non blocking write If sender CFSM module sends faster than receiver can receive events may be overwritten lost Rendezvous Based Communication Start with a rendezvous based specification safe events do not get lost inefficient senders have to wait until receivers are ready before sending more data Relax to bounded buffers wherever possible use minimal buffer sizes maintain lossless communication preserve input output behavior Overview FSM2 CFSM4 CFSM3 FSM4 FSM3 CFSM1 CFSM4 CFSM2 FSM1 CFSM2 CFSM1 CFSM3 Sizing Buffers Translate each CFSM module into an FSM using translator in Polis If state transition times are different normalize the transition time by adding intermediate states A 10 A 15 20 E E 10 20 B 5 C 5 D C B D Sizing Buffers Model each buffer as a FSM Compute the set of reachable states of the network from the transition relations using implicit state enumeration techniques R0 R k 1 R0 V x i Rk T x i y R Rk if R k 1 Rk Sizing and Verification of Communication Buffers for Communicating Processes by Tilman Kolks Bill Lin and Hugo de Man Sizing Buffers Derive the set of reachable states for each communication buffer Determine the minimum buffer size from the reachable states of the buffer Clock Handling Define a global clock Gc with frequency equal to the least common multiple of all frequencies fi fi clock frequency of FSM Fi A FSM makes a transition only when it is active original transition i s s replace by i activei s s i activei s s Buffer Modeling Model buffers as counters FSMs start with an estimated size for each buffer increment buffer on write decrement on read Initial buffer offset 0 next state function adder subtracter add an output function to the buffer B i iover 1 iff an overflow condition occurs expand the counters dynamically during state traversal when necessary Reachable Buffer States Build transition relations for every FSM Fi and buffer Bk Build the transition relation TC of the product machine over variables of the network Obtain the reachable state set from TC Expand the counters buffers dynamically during the state space traversal by adding an additional state variable if an overflow occurs Minimum Buffer Size Derive the set of all reachable buffers states by existentially quantifying over all non buffer state variables Derive the set of reachable states for a particular buffer by existentially quantifying abstracting out the other buffer states Determine the minimum buffer size from the largest value of the counter state Mixed HW SW Implementation with CPU Contention If several processes are sharing a CPU there may be contention due to resource sharing Sender Receiver Therefore we need to modify the buffer sizes to accommodate this case CPU Contention Assume the CFSM network is a DAG and there are no feedback signals To obtain safe minimum buffer size assume all the modules before and including the sender send at the fastest rate possible i e get CPU right when it wants to execute receiver receives at the slowest rate i e at end of queue every time it wants to execute Size buffer one at a time HW SW SW with CPU contection CPU Contention Build the reachable states table for processes that are sharing the same CPU P1 P2 P3 Assume scheduler is FIFO For each state in an FSM S1 S2 S3 S1 S2 S3 S1 look at the possible states that other FSMs can be in and put those processes in the front of the queue Compute worst case waiting time CPU Contention Compute worst case execution time original execution time worst case waiting time and update the transition times in the original FSM For each FSM again normalize the transition time by adding intermediate states Apply the buffer sizing algorithm on the normalized FSM s CPU Contention A 20 A 30 40 E E 20 40 B 10 C 10 D C B D Issues Abstraction State explosion problem during implicit state enumeration One solution abstracting away non buffer variables during state traversal may lose relevant information for buffer sizing when environment is control dominated in which events depend on both time and value need to abstract away variables in a smart way Issues Environment Modeling In original buffer sizing algorithm no assumption is made about the environment Approach is very conservative and buffers may be oversized Hard to model the environment Possible solution given all properties of the environment or test vectors of all possible input patterns model the environment as an FSM and then apply the algorithm in the paper Conclusions We presented an algorithm to find minimumsized buffers between CFSM modules while maintaining lossless communication The case of CPU contention has been considered
View Full Document
Unlocking...