text:
New chp-spec library released
I recently published a multi-part guide on how to provide a mirror implementation of (most of the API of) CHP that spits out a CSP specification of the program rather than execute it. You can go back and read:
- part 1: representing a specification and modelling parallelism,
- part 2: pretty-printing the CSP specification, and calculating parallel alphabets,
- part 3: modelling choice and lifted IO actions,
- part 4: modelling communication, and tracking communicated values, and
- part 5: modelling iteration — processes that repeat their behaviour.
This is the final post I plan to make on the matter (at least for a while)! This post is to announce the release of the work in the above guide as a new chp-spec-1.0.0 library. If you aren't interested in formal specification, and just want to use CHP, you can ignore the chp-spec library. (And if you don't use CHP, you can definitely ignore it!) It's only useful if you want to try to generate a CSP model of your CHP program — and even then, the technique comes with a lot of caveats. But I'd rather release it than leave it sitting on my hard drive.
To use the chp-spec library in place of chp, you must do the following:
- Change the library dependency from chp to chp-spec when you want to generate a specification. You may be able, in cabal, to have both dependencies listed all the time. Currently there is no chp-spec-plus; if you want this, let me know.
- Change the imports in all your modules from Control.Concurrent.CHP* to Control.Concurrent.CHPSpec* when you want to generate a specification; this can be automated somewhat using preprocessor macros if you want to switch between the two regularly.
- Make sure that all uses of the forever function in your process are changed to CHP's foreverP (this is included in CHP 2.2.0 onwards so you can make this change permanent, even when using plain chp).
- Add the process annotation to all directly recursive processes (again, this is included in CHP 2.2.0 onwards, so you can make this change permanent, even when using plain CHP).
- When you want to generate a specification, change the top-level function from runCHP to specify.
The specify function mentioned in the last point is the top-level call that generates and post-processes the CSP specification. The generation has been mostly covered in previous posts; the generation part of specify is trivial; it annotates the top-level process to be called main, then runs the state transformer to get the altered state with all the processes recorded in it (among other things), which it passes to specify', the function that does all the post-processing:
specify :: Bool -> CHP () -> IO String specify showIO main = specify' showIO <$> execStateT (finSpecT $ process "main" main) emptyCHPState
That showIO parameter will be explained later in the post. The code for specify' is long-winded but not very exciting. It can be split into two aspects:
specify' :: Bool -> CHPState -> String specify' showIO st = render specs ++ declMain where ...
We'll start with the first part of that concatenation. The render call uses the pretty-printing to print the specifications. The specs item is generated from the recorded process by two steps: first, it pulls up any Repeated processes to be top-level recursive processes — modern CSP has no iteration operator — and second, it transforms all the process-ids and communications into strings by uniquely numbering the processes and channel values.
The second part of the concatenation, declMain, declares a main process, named "main". We know, because it's the first process that is encountered, that our top-level process will end up named "main_1", so at the most basic we end up with a line "main = main_1", which wraps up all the numbering in a simpler name. But it can have different behaviour depending on that mysterious "unhideIO" parameter.
CSP's semantics revolve around traces, which are records of the visible actions that a process takes. That visible qualifier is significant: CSP allows for hiding of events. This is particularly relevant in case of our dummy IO events. If we leave them as-is, they will show up in the trace of the process even though they are not really a part of its behaviour — but this does allow us to read traces produced by the FDR tool more easily, as we can see which IO events occurred. So the setting is useful for "debugging" any deadlocks, but these extra events can ruin refinement checks because the process appears to be taking extra events. If you're doing a deadlock check, pass True to keep the IO events visible, otherwise pass False to hide them. That is done by the following code for declMain in the where clause of specify':
declMain :: String declMain = "\nmain = main_1 " ++ (if showIO then "" else "\\ {" ++ intercalate "," (map getName $ Set.toList $ chpIOEvents st) ++ "}" ) ++ "\n" where getName = fromJust . flip Map.lookup events
If showIO is False, the main process will hide (backslash is the hide operator in CSP) all the IO events, to stop them being visible to the outside, and in traces of the main process.
Automatic Model Generation, part 5: Iteration
Previous parts of this guide have shown how to represent and print CSP models, and how to redefine the CHP monad and the primitives for choice, IO and communication in order to generate CSP models from CHP programs. This part deals with the final difficult item: iteration.
Most processes in CHP run in an infinite loop, terminated only by poison. Many are written using the helper function forever, which is defined: forever p = p >> forever p. Consider what happens when we try to generate the model for such a process, e.g. forever (syncBarrier b). We first encounter the syncBarrier and we store in the model that the process would engage in event "b". Then in the forever function we loop round and reach the syncBarrier again, and add on to the model that the process would next engage in "b" again. And so on and so on. An infinite loop in our program would cause an infinite loop in our model generation, rendering it useless. We cannot observationally determine that the program is looping forever; think how our approach could possibly distinguish the above from replicateM_ 1000000 (syncBarrier b) >> syncBarrier c.
Forever in an Instant
To solve this particular problem, we supply a foreverP function in the CHP library and its redefinition. In the original CHP library, foreverP acts as forever. In the forthcoming chp-spec library, it is defined differently: it runs the code once to record the model, then makes a note in the model that this code should have run forever. It also stops further modelling; any code after a call to forever will be ignored in the normal library, and so it should be here, too:
foreverP :: CHP a -> CHP b foreverP p = stopSpecT . liftM (Repeat . snd) . finSpecT stopSpecT :: Monad m => m SpecItem -> CHPSpecT m a stopSpecT m = CHPSpecT $ const $ liftM (\sp -> (error "stopSpecT", (sp :))) m
The stopSpecT makes sure that no further specification is performed after this point. The crucial part is the const which ignores the continuation function — this is something that is easily done with our continuation-passing monad (and is like a short-circuiting error monad).
The above takes care of forever, which is used when the program carries no state around. But other processes have direct recursion and cannot use this function.
Process Annotations
To solve the recursion problem, we introduce a process annotation. The process annotation surrounds a process and captures the value of its arguments. The assumption is made (or rather, a condition is placed on the user) that the process will have the same behaviour (excluding any external input from channels and liftIO functions) when given the same arguments. In a pure language like Haskell, this is reasonable and will commonly be the case. The annotation should be added at the beginning of any process that recurses — when the recursion is performed, the process is modelled iff it has never been run before with these arguments; if it has been run before, its behaviour has already been modelled and recorded, so it is returned directly. Here is the annotation in action, on the security guard from the dining philosophers:
security :: [(Chanin (), Chanin ())] -> CHP () security chans = security' chans 0 where security' :: [(Chanin (), Chanin ())] -> Int -> CHP () security' = process "security" $ \chans satDown -> let (ups, downs) = unzip chans maxSatDown = length chans - 1 in (alt $ [readChannel c >> return (satDown - 1) | c <- ups, satDown > 0] ++ [readChannel c >> return (satDown + 1) | c <- downs, satDown < maxSatDown] ) >>= security' chans
It takes as its first parameter the name of the process — it is user-supplied, but should be unique in the program. The second parameter is the process itself. Here, the process has two arguments — but it could be any number. The process annotation is designed using type-classes so that it can be used with processes that take any number of arguments.
We need to store the arguments that each process took when it was modelled. So we need to store the models in a data structure like Map String (Map Args Model). But Args needs to be a set of differently-typed arguments for each process — we can't statically assign a type to it. If we only supported self-recursion we could probably solve this with phantom type parameters in the monad and so forth, but sometimes, even in Haskell, it is appropriate to use dynamic typing. The Data.Dynamic module supports safe dynamic typing (in that casts from the Dynamic type have a run-time check).
In fact, we don't actually need to store the arguments themselves. What we need to store with a previous model is a function like a -> Bool that says whether the latest parameter is the same as was used for generating the previous model:
type CheckArg = Dynamic -> Bool checkArgs :: [Dynamic] -> [CheckArg] -> Bool checkArgs ds fs | length ds /= length fs = False | otherwise = and $ zipWith ($) fs ds
We create a Process type-class to implement our process annotation:
process :: Process p => String -> p -> p process s = process' True s [] class Process p where process' :: Bool -> String -> [(Dynamic, CheckArg)] -> p -> p instance (Eq a, Typeable a, Process b) => Process (a -> b) where process' topLevel name args f x = process' topLevel name (args ++ [(toDyn x,(== Just x) . fromDynamic)]) (f x)
The process' function takes a Bool (ignore that for now), the process name, a list of arguments so far (each pair is the argument itself, and its function to check against a future value), and then wraps a process "p". The instance shown above is the one that captures all a process's parameters. Each parameter is appended to the list. toDyn turns a value into a Dynamic, and fromDynamic returns a Maybe value (Nothing if the type-cast is unsuccessful, Just if was successful). Comparing the result of fromDynamic to Just x checks both the type and the value at once. To support dynamic typing, parameters must have a Typeable instance (which GHC can derive for most types — and is supplied for all CHP library types) and an Eq instance to check for equality. The most notable types that cannot be used for a parameter are functions. This is a limitation of the approach — and indeed, CSP itself does not support any notion of functions being passed around. Any processes that take functions as parameters would have to be made first-order (Neil Mitchell's Firstify comes to mind).
The base-case instance for Process is the one that actually uses the parameter list:
data CHPState = CHPState { ... , chpProcessMap :: Map.Map String (Map.Map Integer ([CheckArg], (Spec,Dynamic))), chpFreeNames :: [(Dynamic, CheckArg)], chpNextProcess :: !Integer } instance (Typeable a, Eq a) => Process (CHP a) where process' topLevel name immArgs p = addSpecT1 $ do st <- get let possibles = Map.toList <$> (Map.lookup name $ chpProcessMap st) args = if topLevel then immArgs else chpFreeNames st ++ immArgs case possibles >>= L.find (checkArgs (map fst args) . fst . snd) of Just (n, (_, (_, r))) -> return (flip fromDyn (error "process-lookup") r, Call n) Nothing -> do let n = chpNextProcess st put $ st { chpProcessMap = insertMapMap name n (map snd args, (error "process", toDyn ())) $ chpProcessMap st , chpFreeNames = args , chpNextProcess = succ n } (r, f) <- finSpecT p modify $ \st' -> st' { chpProcessMap = insertMapMap name n (map snd args, (f, toDyn r)) $ chpProcessMap st' -- Restore original free names: , chpFreeNames = chpFreeNames st } return (r, Call n)
The case statement checks if any previously-modelled processes match. If one does (the Just case), its model and return value are returned. If Nothing is found, the process is modelled. It is crucial that the state is first updated with an entry for the process — that way, when the process recurses, it can find itself in the collection of recorded processes (if the recursion uses the same argument values). The dummy entry has the right parameters but an invalid model (that will never be accessed before it is later updated) and an incorrect return type; processes that recurse and then examine the value of the recursive call are not supported here. However, almost every recursive CHP process is tail-recursive, which can be modelled just fine (if they weren't tail recursive, they would probably feature a space-leak). After the process has been modelled, its entry is updated with the real return value and real specification.
The model returned by the process annotation is always simply a Call item. Therefore, any process that recurses will simply have a Call item added to the end, stopping the model from extending forever — provided that at some point the same parameters are used to the process. A parameter with continually-changing parameters that never repeat — for example, one that outputs ascending integers — cannot be modelled here. This is yet another limitation of the approach.
As an example, we'll use the security guard shown earlier in this post, and how that is modelled with three philosophers (i.e. three sets of channels). Our approach produces a model for each different set of arguments to the process — the models for different arguments can potentially be completely different. Some effort could be put into collapsing them back down during post-processing, but here are the three models:
security_10= (((security.up.phil0?x_14 -> security_9) [] (security.up.phil1?x_15 -> security_9) [] (security.up.phil2?x_16 -> security_9) [] (security.down.phil0?x_17 -> security_11) [] (security.down.phil1?x_21 -> security_11) [] (security.down.phil2?x_22 -> security_11))) security_11= (((security.up.phil0?x_18 -> security_10) [] (security.up.phil1?x_19 -> security_10) [] (security.up.phil2?x_20 -> security_10))) security_9= (((security.down.phil0?x_13 -> security_10) [] (security.down.phil1?x_23 -> security_10) [] (security.down.phil2?x_24 -> security_10)))
The top process, security_10, is the state where one philosopher is currently seated and thus all up and down events are offered. If an up event occurs, the next process is security_9, the state where no philosophers are seated, and thus only down events are offered. If a down event occurs in security_10, the next process is security_11, where two philosophers are seated and only up events are offered: this prevents a third philosopher sitting down (which could potentially lead to the classic deadlock in the dining philosophers).
That concludes all the in-depth technical parts of this guide. There'll be one more post explaining the top-level specify method, which should also include the announcement of the release of the chp-spec library based on this guide.
Automatic Model Generation, part 4: Communication
This is part of a multi-part guide on redefining the CHP monad and primitives to generate a CSP model rather than executing the program. In this relatively self-contained part, we examine the issue of tracking values as they are communicated around the process network.
Modelling the mere occurrence of communications and synchronisations themselves is quite straightforward. We just label each created channel/barrier with a unique identifier, and then every time it is used we record in the model which channel/barrier was used. We can, however, do a bit better than that. Consider this code:
do x <- readChannel input writeChannel output x
What if we could tell that the value sent on the output channel was the same value as the one received on the input channel — that would be much more powerful than simply recording that a communication took place on the input channel followed by a communication on the output channel.
Identifiable Bottoms
Haskell has a function, undefined :: a. This produces a "bottom" value of any type, and will give an error if evaluated. It has a counterpart, error :: String -> a that allows the error message to be customised to be something useful. The Control.Exception module provides a try function that can catch these messages, and an evaluate function to examine values. If we put all of these together, we can create dummy values of any type, and later on we can identify them (but see the limitations section at the end of this post). This is the same technique used by Lazy SmallCheck, which we used for modelling IO computations in the previous part of the guide.
Input and Output
When an input occurs, we use the identifier of the channel (which is passed to the fakeCommIn function below) to form a uniquely-identifiable bottom value, which we make a note of in our state and then return:
bottomPrefix :: String bottomPrefix = "__CHP.bottom__" fakeCommIn :: Integer -> CHP a fakeCommIn n = addSpecT1 $ do st <- get put $ st { chpNextBottom = succ (chpNextBottom st) } return ( error $ bottomPrefix ++ show (chpNextBottom st) , Sync $ Right (n, DirInput, chpNextBottom st) )
The Sync . Right item holds the identifier of the channel, "n", the direction of the communication, and the identifier of the bottom value involved. In our corresponding output function, we watch out for these bottom values:
fakeCommOut :: Integer -> a -> CHP () fakeCommOut n x = addSpecT1 $ do possErr <- lift $ C.try $ C.evaluate x case possErr of Left (C.ErrorCall s) | bottomPrefix `isPrefixOf` s -> return ( (), Sync $ Right (n, DirOutput, read $ drop (length bottomPrefix) s)) -- Wasn't one of our bottoms: _ -> return ((), Sync $ Left n)
That is all the core code we need. Our replacement channels just store the channel identifier, and delegate reading and writing on channels to the above two methods.
For an example, we will use a process that reads two values from one pair of channels, and sends them out, swapped, on another pair of channels:
import Control.Concurrent.CHPSpec import Control.Monad (replicateM) swap :: (Chanin a, Chanin b) -> (Chanout b, Chanout a) -> CHP () swap (inA, inB) (outB, outA) = do (a, b) <- readChannel inA <||> readChannel inB writeChannel outB b <|*|> writeChannel outA a p :: CHP () p = do leftIn <- oneToOneChannel' $ chanLabel "leftIn" leftOut <- oneToOneChannel' $ chanLabel "leftOut" rightIn <- oneToOneChannel' $ chanLabel "rightIn" rightOut <- oneToOneChannel' $ chanLabel "rightOut" swap (reader leftIn :: Chanin Int, reader rightIn :: Chanin Int) (writer leftOut, writer rightOut) main :: IO () main = specify True p >>= putStrLn
This program is able to generate the following model, that correctly follows the values through the process:
channel leftIn channel leftOut channel rightIn channel rightOut main_1= (((leftIn?x_1 -> SKIP) ||| (rightIn?x_2 -> SKIP)) ; ((leftOut!x_2 -> SKIP) ||| (rightOut!x_1 -> SKIP)))
The technique of identifying bottoms is far from foolproof. In particular, for Int, "1+x" will be identified as being the same as "x". What we are really identifying is that the bottom value received is used somewhere prominent in the output. So the idea is nice, but the execution is imperfect. Tristan Allwood suggested looking at stable names — these may help to reduce the imperfection, but they do not provide a strong enough guarantee to make the technique water-tight either.
I have now covered most of the model-generation technique. In the next part I will tackle the complex matter of recursive processes, probably followed by a final part showing how the top-level specify method works — at which point I hope to release all of this as a library, alongside the next CHP release (with the mtl dependency removed).
Automatic Model Generation, part 3: Choice and IO
This is the third part in a multi-part series describing a technique to generate formal CSP models of CHP programs by redefining the CHP monad and primitive actions to output the model of the program. In part 1 we saw the redefinition of the monad and the specification type; in part 2 we saw how to pretty-print the model, including the parallel composition alphabets. In this part, we look at choice and IO actions.
In part 1 of this guide, we saw how to define parallel composition. The specifications for each branch were generated, composed into a Par item, and added to the model. Choice is not so straightforward, because it can introduce branching execution paths. Consider this code:
alt [syncBarrier b >> return Nothing, syncBarrier c >> return (Just x)] >>= maybe p q
The choice doesn't return a single value — it returns one of two, and which value is returned will affect the code coming afterwards. So we need a different approach from just putting a choice on the front of the sequential execution of the model. In fact, there is quite a simple solution just by using one of the laws of CHP from the tutorial:
alt [p, q] >>= k = alt [p >>= k, q >>= k]
This rule is usually useful because you can use it to remove the code duplication on the right by transforming to the form on the left. Here, we will use the rule in the opposite way, to move the binding of the multiple results back into the alt and attach it to each branch.
The alt :: [CHP a] -> CHP a function chooses between several alternatives. We define it by using the Alt specification item:
alt :: [CHP a] -> CHP a alt [] = stopSpecT $ return Stop alt ps = altSpecT ps altSpecT :: Monad m => [CHPSpecT m a] -> CHPSpecT m a altSpecT ms = CHPSpecT $ \k -> do xfs <- mapM (flip runSpecT k) ms return (error "alt return", \s -> [Alt $ map (($ s) . snd) xfs])
The key aspect of this code is that due to the continuation-passing style of the replacement CHP monad, we have a continuation ("k" in the above code) that represents all actions that would be taken after the alt. We pass this as the continuation when we run each of our branches of the alt (the first line of the do block). The specification-modifying functions from each branch are applied to future specifications, then returned as a specification containing a single Alt item. This can be depicted as follows:
Note that the eventual return values of all of the branches are discarded. This is not as bad as first appears, because the result values are only used if this choice is in a parallel composition and its result is needed (which is surprisingly rare in CHP code) or if the choice is in a recursive process where the result is needed (this again is surprisingly rare, and will be dealt with in a future part of the guide).
IO Actions
The real CHP monad is really a monad transformer on top of the IO monad, and supports IO actions being lifted into the CHP monad. An IO action may perform all sorts of actions, but these fall outside the scope of our modelling. The more significant problem for the modelling is that the IO actions may return a meaningful value (i.e. one other than a unit return). These values can then be used in the CHP program, and in particular they may be used to branch execution. If we simply return an error value in these cases, the code will fail. We can do slightly better than that, to allow partial support for IO actions when modelling.
In the case of an IO computation, we have some code (the code following the IO computation) that takes a value (the return value of the IO computation) and produces an output based on the value (the model of the code following the IO computation). This is, in effect, a testing problem, and we can borrow techniques from software testing to solve it. Haskell has several clever testing libraries: QuickCheck is one of the most well-known, but an even cleverer library is Lazy SmallCheck. Lazy SmallCheck allows for an efficient search of the input space to a function by starting off with undefined values, and partially defining them as necessary. Not only can this be efficient, but a particularly nice aspect is that it allows us to know if the search was complete or not.
The Lazy SmallCheck library doesn't actually expose enough of its implementation as it currently stands, so I took it and modified it until I was able to produce a fuzz function:
fuzz :: (Serial a) => (a -> StateT s IO b) -> StateT s IO ([b], Bool)
This function takes an IO computation that sits inside a state monad transformer (I needed this, and it was much easier to embed this in the fuzz function than to do it any other way). The input space for this function is searched (with the stateful side-effects of any successful returns being kept) and a list of return values (the models) is produced. The boolean parameter indicates whether the search was complete: that is, whether it examined all possible values in the search space (either by exhaustion of all fully-defined values, or because it explored a complete set of partially defined values).
We can use the fuzz function on the continuation passed to the IO computation in order to explore the continuation's possible models with different input values to the continuation. This will give us a collection of models, each of which represents a possible behaviour of the program from this point, based on an event (the IO action) that we must treat as unpredictable and out of our control. In CSP we can join these models together as an external choice between processes that are prefixed with non-synchronising events: that is, events that are not featured anywhere else in the model. The external choice between such events indicates that the process's behaviour will depend on which event is offered by its environment, and that we must assume that any event might be offered (i.e. any input value might be returned). This code achieves that:
liftIO_CHP :: Serial a => IO a -> CHP a liftIO_CHP _ = CHPSpecT $ \k -> do (vals, complete) <- fuzz k unless complete $ liftIO $ putStrLn "Incomplete fuzzing of IO computation" nonces <- replicateM (length vals) newEvent let firstLabel = "IO_" ++ show (head nonces) zipWithM_ labelEvent nonces (map (firstLabel++) suffixes) modify $ \st -> st { chpIOEvents = Set.union (Set.fromList nonces) (chpIOEvents st) } return (error "liftIO return", \s -> [Alt $ zipWith (\n f -> Sync (Left n) : snd f s) nonces vals]) where suffixes = map (:[]) ['A'..'Z'] ++ map show [(0::Integer)..]
As ever, this technique is limited: the search may be incomplete, in which case the model may be incomplete. We print a message in these cases to warn the user of the problem. The search will only be incomplete if the return value has a large flat domain (e.g. integers) and/or the subsequent computation makes full use of the domain. If the return value is ignored or if it is not used to make decisions about the control path, the search will be complete (because the value will never be defined). So if, for example, a String is returned and then passed to a different IO action to write to a file, this will not cause a problem in the modelling because the behaviour in terms of CSP processes is invariant to the return value. The only time this search above comes into play is when the return value is used to affect the execution path, for example if the process acts differently when the String is empty. (This is reminiscent of the different between monads and applicative functors: if CHP was only an applicative functor, IO actions could be completely ignored.)
For an example, I will use a simple simulation example with a tick-tock barrier to divide time into time-steps. The simulation has six site processes wired up in a ring, with each site connected to its neighbours via a pair of barriers, representing incoming and outgoing movements. A site may be full or empty. If it is full (i.e. contains an agent), it makes a random choice as to which direction to send the agent in a time-step (and then ends the time-step). If it is empty, it offers to receive a new agent from either side, or to end the time-step. Here's the diagram (the star indicates a full site) and the code:
site :: EnrolledBarrier -> (EnrolledBarrier, EnrolledBarrier) -> (EnrolledBarrier, EnrolledBarrier) -> Bool -> CHP () site = process "site" $ \bar (inL, outL) (inR, outR) occupied -> (if occupied then do shouldMove <- liftIO_CHP' "shouldMove" $ getStdRandom random if shouldMove then do moveLeft <- liftIO_CHP' "moveLeft" $ getStdRandom random if moveLeft then syncBarrier outL else syncBarrier outR syncBarrier bar return False else syncBarrier bar >> return True else alt [syncBarrier inL >> syncBarrier bar >> return True ,syncBarrier inR >> syncBarrier bar >> return True ,syncBarrier bar >> return False ] ) >>= site bar (inL, outL) (inR, outR) main :: IO () main = specify True (runSiteRing [True, False, False, True, False, False]) >>= putStrLn
I've omitted a couple of uninteresting wiring functions. You can see that I'm using a version of liftIO_CHP that allows me to supply a label, which helps in reading the model. The program uses choice, and lifted IO actions to get random boolean values. It also has a potential deadlock, which we will find using the FDR model-checker.
One problem with this whole technique at the moment is that each site generates a separate model, even though they are all similar enough to be expressed in one model. So here are the processes that make up the behaviour of the first site — there are similar pairs for the other five sites:
site_2= (((IO_shouldMove7A -> tock -> site_2) [] (IO_shouldMove7B -> ((IO_moveLeft5A -> right_0 -> tock -> site_3) [] (IO_moveLeft5B -> left_5 -> tock -> site_3))))) site_3= (((right_5 -> tock -> site_2) [] (left_0 -> tock -> site_2) [] (tock -> site_3)))
The site_2 process is the full process. It makes a choice between two events: IO_shouldMove7A and IO_shouldMove7B. These are the two possible outcomes of asking for a random boolean. In one case, it synchronises on the tock event and recurses — this must be the won't-move case. In the other, it chooses between two other events: IO_moveLeft5A and IO_moveLeft5B. These are the decisions as to whether to go right or left: it next either synchronises on its right event or its left event, and then becomes site_3. The site_3 process is the empty process. It will agree to synchronise with its neighbours, end the timestep and become the full process — or to just end the timestep and remain the empty process.
There are six such pairs of processes in the model, one for each site in our model. The only difference between them is the names of the dummy IO events, and the numbers of the right and left events. They are all wired up in the main process:
main_1= (((site_2) [|{| left_0 , left_5 , right_0 , right_5 , tock |}|] (((site_4) [|{| left_4 , right_4 , tock |}|] (((site_6) [|{| left_3 , right_3 , tock |}|] (((site_8) [|{| left_2 , right_2 , tock |}|] (((site_10) [|{| left_1 , right_1 , tock |}|] (site_12)))))))))))
We can add a single line at the end of the model: assert main_1 :[ deadlock free] and feed it to FDR, asking it to produce a trace if it finds a counter-example. FDR does find a counter-example for our assertion: a trace that ends in deadlock. Here it is:
IO_shouldMove7B IO_moveLeft5A right_0 IO_shouldMove25A tock IO_shouldMove35B IO_moveLeft33A right_1 IO_shouldMove25B IO_moveLeft23B
We can take this trace (a chronological list of events that occur) and relate it to the model. Here's the short form: the agent in the first site moves right, while the agent in the fourth site stays put, and the time-step ends. Then the agent that is now in the second site moves right, and the agent in the fourth site decides to move left. At this point, one agent is in the third site (which is waiting to end the time-step) and the other is in the fourth site trying to move into the third site. Deadlock!
There are several ways to solve this problem, but I'm not really interested in them — the point here was to show that we took a simple example, we generated our model and fed it straight to the proof-checker which gave us a trace that produces deadlock. Reading the CSP and relating the trace to the model is straightforward, but can be long-winded. What might be nice in future is to have an option to somehow encode the source location in the event name, to then easily point back to the source and say "this bit of the source happened, then that bit happened, then deadlock". In the next part of the guide I'll show how we can deal with tracking communications when building the model.
Automatic Model Generation, part 2: Pretty-Printing the Model
In the first part of this guide, I explained part of a technique for generating CSP models from a CHP program — including the introduction of the specification type. In this second part of the guide I take a slight diversion to explain how to pretty-print the specifications. We will see in this part how parallel composition is rendered, which has particular importance in CSP.
After we've created the model of our program, we need to print it out to a file, ready to be fed to the proof-checker or other tool. I wanted the model to be as comprehensible as possible after printing, so that users (and I!) can read it. To that end, I used a pretty-printing library: pretty from Hackage, which is imported as PP throughout the code in this post. (After I wrote this code, Marc Fontaine uploaded a library to Hackage produced that supports CSP notation in an AST, but it's easier for me to keep my original code rather than switch over.)
CSP has two forms of sequencing. A semi-colon sequences two processes, whereas an arrow prefixes a process (right-hand side) with an event (left-hand side). My code for printing out a sequence of processes uses the arrow wherever possible, and a semi-colon otherwise:
type ProcEvents = Map.Map String (Set.Set String) pprintCSP_Seq :: ProcEvents -> Spec' String String -> PP.Doc pprintCSP_Seq m = PP.parens . PP.sep . p where p [] = [PP.text "SKIP"] p (Sync c : xs) = [name c, PP.text "->"] ++ p xs p [x] = [pprintCSP m x] p (x:xs) = [pprintCSP m x, PP.text ";"] ++ p xs
The SKIP process does nothing, so it is used for blank lists and at the end of the list. Note that the singleton list [Sync x] will turn into x -> SKIP, whereas [Par xs] will not turn into xs ; SKIP (it will be merely xs). The ProcEvents parameter is used later on for printing out parallel composition and so must be passed around in case there are any nested parallel compositions.
External choice is handled by the first case of pprintCSP:
pprintCSP :: ProcEvents -> SpecItem' String String -> PP.Doc pprintCSP m (Alt s) = zeroOneMore m "STOP" (withOp m "[]") s
The helper functions are used to treat differently the case where the list is empty (in which case it uses the second parameter), has one item (in which case it is printed using pprintCSP_Seq), or has multiple items (in which case it is processed using the third parameter, which above joins the items with the external choice operator []):
withOp :: ProcEvents -> String -> [Spec' String String] -> PP.Doc withOp m op = PP.parens . PP.sep . intersperse (PP.text op) . map (pprintCSP_Seq m) zeroOneMore :: ProcEvents -> String -> ([Spec' String String] -> PP.Doc) -> [Spec' String String] -> PP.Doc zeroOneMore _ z _ [] = PP.text z zeroOneMore m _ _ [x] = pprintCSP_Seq m x zeroOneMore _ _ f xs = f xs
When you compose two CSP processes in parallel, you must specify the events on which they synchronise. The process (a -> SKIP) [| {|a|} |] (a -> SKIP) will perform the event "a" once, with both sides of the parallel synchronising on event "a" together — that item in the middle is an infix parallel composition operator, parameterised by the singleton set containing "a". In contrast, the process a -> SKIP [| {| |} |] a -> SKIP (which can be written more simply as: a -> SKIP ||| a -> SKIP) will perform the event "a" twice, with each side of the parallel doing it in turn — this is known as interleaving on an event.
In CHP, there is no support for interleaving; all events are synchronising. However, we cannot just put all events in the synchronising set. The process (a -> SKIP) [| {|a,b|} |] (b -> SKIP) will deadlock — each side tries to synchronise with the other on their respective events, which never happens. The solution is of course to use the intersection of the events that each side engages in:
pprintCSP m (Par xs) = zeroOneMore m "SKIP" joinPar xs where joinPar :: [Spec' String String] -> PP.Doc joinPar [a] = pprintCSP_Seq m a joinPar (a:bs) = PP.parens $ PP.sep $ [ pprintCSP_Seq m a , pprintParOp (findAllComms eventName m a `Set.intersection` unionAll (map (findAllComms eventName m) bs)) , joinPar bs ] pprintCSP _ (Call p) = name p pprintCSP _ x = error $ "pprintCSP: " ++ show x pprintParOp :: Set.Set String -> PP.Doc pprintParOp s | Set.null s = PP.text "|||" | otherwise = surround "[|{|" "|}|]" $ intersperse PP.comma $ map name (Set.toList s) where surround a b x = PP.sep $ [PP.text a] ++ x ++ [PP.text b]
The findAllComms does as its name suggests: it forms a set of all the communications performed anywhere in the process, using the supplied Map that we have been passing around to find out what communications are performed by named processes that are called. Note that as we compose parallel items together, we compose the head of the list using the intersection of all communications performed in the head, and all communications performed in the rest of the list (which will be the right-hand side of the parallel composition). So if you have three processes: [a -> b -> SKIP, b -> c -> SKIP, a -> c -> SKIP], they will get composed as:
(((a -> b -> SKIP) [|{| a , b |}|] ((b -> c -> SKIP) [|{| c |}|] (a -> c -> SKIP))))
The first process synchronises on "a" and "b" with the others, as both feature somewhere later in the list. The second and third process only synchronise together on "c"; the events "a" and "b" are not shared, and thus occur separately, but synchronised with the first process.
Parallel Composition Omission
Basing the synchronisation sets on those events that are potentially performed has a problem. If a process is given a channel-end or barrier, but never uses it at all, the event will not show up in the model for that process, and thus will not be used in the synchronisation set. Let's say you have a barrier, "b" with two processes enrolled, but one does not use it. Given those two processes, say "a ->SKIP" and "SKIP" they will be composed as "a ->SKIP ||| SKIP", which will run fine — even though the original program would have deadlocked! The solution to this is to introduce extra code for tracking how many processes are involved in an event, and add dummy processes that have the events in their synchronisation set but never use them, thus reflecting the deadlock in the model. I haven't yet implemented this just yet, though.
We have now seen how parallel composition is implemented, including determination of the synchronisation sets. In future parts of the guide, we will examine the remaining parts of CHP: channel communications, choice, and iteration, as well as how all these are put together.
Automatic Model Generation, part 1: Parallel
CHP is based on CSP, a formal process calculus. CSP has a model-checker, FDR (among other tools), that is free for academic use for dealing with CSP. It would be great if we could take our CHP programs and prove them correct using FDR, e.g. prove them deadlock free. To properly translate a CHP program into its CSP model requires full semantics-based processing of the program's source code, including all the functional parts (including tackling things like writeChannelStrict c undefined). But what if, at least for simple programs, we didn't need to go to these lengths?
In this multi-part guide, I will introduce a technique to generate CSP models from CHP programs without source code analysis. The programmer would make one small alteration to the imports of a program and then: instead of executing properly, the program would spit out its own CSP model which we could feed to FDR. This technique involves redefining the CHP monad and all the CHP primitives so that the program spits out its model rather than actually executing. The technique is very limited in some regards, and I'll try to point out the limitations as we go along. But hopefully it will be interesting to show what you can do by redefining your monad (see also: the Concurrent Haskell Debugger, and the Beauty in the Beast paper). Explaining my technique will take several posts — for today, I will focus on the definition of the specification type, the CHP monad — and redefining the runParallel function.
Specification Type
We start by defining a type to represent a CSP model. An introduction to CSP can be found in a previous post, but if you know CHP then the CSP model type has a fairly straightforward correspondence to CHP code. The type of the specification is as follows:
data SpecItem' proc comm = Par [Spec' proc comm] | Alt [Spec' proc comm] | Call proc | Sync comm | Stop | Repeat (Spec' proc comm) deriving (Show) type Spec' proc comm = [SpecItem' proc comm]
The main Spec' list type is a chronological sequence of processes in the model. The types are parameterised by proc (the type that identifies a process) and comm (the type that identifies a communication/synchronisation). We will explain these types in a future part of the guide; for now, we will use the opaque types ProcessId and CommId:
type SpecItem = SpecItem' ProcessId CommId type Spec = Spec' ProcessId CommId type SpecMod = Spec -> Spec finalise :: SpecMod -> Spec finalise f = f []
The SpecMod type is a function that modifies a specification. We will compose several of these functions while building the model — and at the end, we can use the finalise function to turn a SpecMod function into an actual Spec, by applying the function to the empty sequence.
Redefining the CHP monad
These specification types are used in our redefinition of the CHP monad. The main part of the new CHP monad is a monad transformer CHPSpecT that permits building of specifications on top of an existing (book-keeping) monad. The monad is as follows:
newtype CHPSpecT m r = CHPSpecT {runSpecT :: forall b. (r -> m (b, SpecMod)) -> m (b, SpecMod) }
For those of you playing monad transformer bingo at home, CHPSpecT is effectively the unrolled version of forall b. ContT b (WriterT SpecMod), and will later be used on top of StateT. As with ContT, the monad instance itself makes no reference to the underlying monad, so it is surprisingly simple:
instance Monad m => Monad (CHPSpecT m) where return x = CHPSpecT ($ x) m >>= k = CHPSpecT $ \c -> runSpecT m $ \a -> runSpecT (k a) c
The road to hell is paved with monad explanations, but here goes. The r -> m (b, SpecMod) item takes a value of type "r" (for red) and gives back an item of type "b" (for blue) along with a specification modifying function. We can envisage that item as follows:
The values pass left to right in the top half (turning red to blue), while the model actually passes in the opposite direction. Our models are effectively built backwards, with each SpecMod function modifying all future specifications to produce a current specification. We can now diagram our CHP monad as follows:
Given a circled value of the aforementioned type r -> m (b, SpecMod) (the lambda is used to indicate that this is an argument), a CHP item will give back something of type m (b, SpecMod); this is drawn on the right as a blue item with a straight left edge (to indicate it has no input), paired with a specification-modifying function. You can pick all sorts of holes in these diagrams, but I hope they will be useful in explaining various uses of this monad as the guide continues.
CHP Monad Helper Functions
The CHP monad itself has no real logic involved; all the logic is actually captured in other functions, two of which I will introduce here, beginning with finSpecT:
finSpecT :: Monad m => CHPSpecT m r -> m (r, Spec) finSpecT = liftM (second finalise) . flip runSpecT (\x -> return (x, id))
The finSpecT function is used to run the CHPSpecT transformer; it returns a value and a model. Once it has the return value paired with the corresponding model-changing function, it makes the latter into a model by finalising it (applying it to the empty specification). The result of this latter operation can be visualised below; the composite item has an unmodified return value, but has its specification-modifying function applied to the empty specification (the empty list):
The second function is addSpecT1:
addSpecT1 :: forall m r. Monad m => m (r, SpecItem) -> CHPSpecT m r addSpecT1 m = CHPSpecT $ \k -> m >>= apply k where apply :: (r -> m (b, SpecMod)) -> (r, SpecItem) -> m (b, SpecMod) apply k (x, s) = liftM (second ((s :) .)) $ k x
The addSpecT1 function encapsulates the logic for sequencing; it takes a monadic action that gives a return value paired with a corresponding single specification item, and turns all that into a CHPSpecT item that adds the item to the model. The diagram is below; the addSpecT1 takes a parameter (the outermost lambda) and gives back a CHP item that takes an inner continuation parameter (the lambda inside the box). The value of the outer parameter is passed to the continuation, and the specification item of the outer parameter (a trapezoid named "s") is adjoined to the front of the result of the specification-modifying function of the continuation:
Parallel Composition
For parallel composition, we take each branch of the parallel composition and finalise it into a specification (using finSpecT), then add the Par constructor and join it on to the front of future specifications:
runParallel :: [CHP a] -> CHP [a] runParallel = addSpecT1 . liftM (second Par . unzip) . mapM finSpecT
We can again diagram this:
Hmmm, hopefully that makes it clearer! The finalised parts of the parallel specification (which were run sequentially — no need for actual parallelism during model generation) are shown on the left: their return values are formed into a list of values (following the arrows at the top of the diagram) that is passed to the continuation, while their models are put into a list with a Par constructor (following the arrows at the bottom of the diagram), and this is prepended to the sequence from future models.
We can now given an example of the model generated for a program with parallel composition. This example is particularly simple, as I don't want to use features that I haven't yet explained. Here is a plain CHP program, that synchronises on various barriers in parallel:
import Control.Concurrent.CHP syncOn :: [String] -> CHP () syncOn = mapM_ syncOnIndiv where syncOnIndiv :: String -> CHP () syncOnIndiv name = do b <- newBarrierWithLabel name enroll b syncBarrier p :: CHP () p = runParallel_ [syncOn ["a", "b"], syncOn ["c", "d"], syncOn ["e"]] main :: IO () main = runCHP_ p
This program will compile, and can be executed normally. To get a model of this program, rather than executing it, we only need change the top and bottom lines; we import a different module, and change the outermost-call to runCHP_ to specify:
import Control.Concurrent.CHPSpec ... processes as before main :: IO () main = specify True p >>= putStrLn
The program will again compile (against a different library), but this time when it is executed it will output the following model, ready to be read into the FDR model-checker or another formal tool for CSP:
channel a channel b channel c channel d channel e main_1= (((a -> b -> SKIP) ||| ((c -> d -> SKIP) ||| ((e -> SKIP))))) main = main_0
In the next part of the guide, we will examine exactly how these models are printed — and after that we will cover model generation for CHP's other primitives.


text:
Subscribe to FoMMP 50-50 CLUB!
0 Members and 1 Guest are viewing this topic.
At no point did I suggest otherwise - the closest I got was pointing out that people like nice new buildings. They may not perform better, but good working conditions are well known to be a factor in hanging on to good staff.
THe conditions where people are has little correlation to performance, Elton Mayo's experiments prove this.
If the NPV of savings is greater than the cost of demolition and rebuild, surely the college will do that anyway, regardless of selling the site.
At Cheadle, as at Marple, the college initially operated in two former school buildings. About ten years ago it had the good fortune to discover that one of them was unsafe because of reinforced concrete decay, and it had to be demolished. It therefore had to be replaced, hence the smart and efficient new building which students use on the Cheadle site.The other building at Cheadle (the former girls' grammar school) is also still in use, although I believe it has had some modernisation work. It is only about 50 years old - whereas the Hibbert Lane building dates from 1931.I entirely agree that quality of teaching, college standards and student care are very important. But in reality, these factors improve as a result of replacing inefficient old buildings with efficient new ones, because funds are released to improve them. And it isn't really about 'shiny new rooms' at all, though students do like them, and so do staff - and attracting and retaining the best staff is key to providing a quality education.However, the key factor is cost and efficiency. Having managed a college which moved from grotty old converted buildings to shiny new purpose-built ones, I can tell you that the savings in running costs (heating, lighting, maintenance) and in space efficiency were astonishing, and of course they are savings which recur, year in, year out, and become really significant. And this enabled us to free up much needed resources to help improve the teaching.
Now, how do you "improve teaching" with money? is that by getting more expensive teachers? i didnt really think that was possible!
In the end actually i think it is about leadership, a good manager always brings the best out of their staff regardless of the facilities!
Yes. Striving to provide the best possible facilities for your students, and ensuring that scarce resources are directed towards funding teaching rather than maintaining out-of-date and inefficient buildings, is exactly what a socially responsible educational organisation should be doing.
QuoteThe college is trying to improve its buildings for the benefit of our children and grandchildren. A noisy and self-appointed group of campaigners is trying to stop them, and in the process is, at times, spreading misinformation.It could also be said that the college, which is supposed to be a part of the local community is waving two fingers at the local community and is behaving in a "I'm all right Jack manner". There is a large number of local children who have made the choice NOT to attend the local college, maybe because they see the college as a socially irresponsible organisation. They (the college) have to earn the right to educate our children, their present stance puts into question if they are a fit body to undertake this.
The college is trying to improve its buildings for the benefit of our children and grandchildren. A noisy and self-appointed group of campaigners is trying to stop them, and in the process is, at times, spreading misinformation.
Do you think that CAMSFC is setting a good example of social responsibility in the way that they have conducted themselves over the last 6 years?
It could also be said that the reason many of our children do not choose to go to the college is because they lack the facilities that other local colleges can provide. They lack these facilities because they have had to spend money over the years on buildings that have been way past their best for a number of years now.
Utter waste of time! What a load of febrile and self-centred nonsense

subset: commoncrawl


text:
Metal Finishing Model Shop Program Successes
Valley Chrome Plating
Valley Chrome Plating of Clovis became successful in California by marketing its bold, stylish line of chrome truck bumpers and accessories to America's big-rig truck drivers.
"Truckers love chrome," says Ray Lucas, president of the firm run by four sons and two daughters of a steelworker dad who bought into it in 1961.
Now the family business is becoming a national industry leader by using safer chemicals in its manufacturing process with no loss in revenue.
Last year, with encouragement of the California Department of Toxic Substances Control, Valley Chrome became one of the first sizeable decorative plating firms in the U.S. to abandon carcinogenic hexavalent chrome in its manufacturing process and switch to less toxic trivalent chrome.
The shift is a key component of Green Chemistry. Replacing dangerous chemicals with safer alternatives protects workers, consumers and the environment while creating new business opportunities.
Valley Chrome, with 80 employees and $10 million in annual revenue, occupies the top 25 percent tier of U.S. metal plating firms.
"I think in 10 years the majority will do trivalent chrome," says Lucas, who served in 2007 and 2008 as president of the National Association of Surface Finishing, a trade group for the $4 billion U.S. industry. "In my opinion, decorative platers will get more pressure about hexavalent chrome."
The switch improved Valley Chrome's bottom line, Lucas said. The substitution cost $170,000 up front, but saved $140,000 by avoiding cost of a hexavalent chrome fume scrubber required by the California Air Resources Board. Trivalent chrome, which doesn't require buffing after the manufacturing process, eliminated the need for two employee positions. Trivalent chrome also coats metal surfaces more efficiently than hexavalent chrome. As a result, the company's product reject rate has fallen to 2.6 percent, compared to an industry average of 7.5 percent.
The K & L Anodizing Story
DTSC awarded K & L Anodizing in Burbank, Calif., the first Metal Finishing Model Shop recognition in September 2005. Besides pride in their accomplishment, here are some of the cost and environmental benefits the company realized by implementing pollution prevention measures and participating in the program.
- Wastewater reductions of more than 95,000 gallons per day by installing a closed loop ion exchange system.
- Extended process bath life of 50 percent using filters and chemical analyses, leading to big operating cost savings from both the purchasing and waste disposal ends.
- Energy and cost savings from installing efficient lighting, insulated and temperature-controlled hot tanks, and a natural gas boiler.
- Free compliance and pollution prevention assistance direct from regulators.
- Public recognition as a Model Shop award recipient. Press Release


text:
(Pocket-lint) - The Amazon Kindle might be the e-book reader that everyone knows, but as it is not available to anyone outside the US, readers in the UK have got to use something else. Is the Booken Cybook Gen3 the answer? We get reading to find out.
Roughly the size of a piece of A5 paper (118 x 188 x 8.5mm), the Cybook Gen3 is light and small and easily portable. The e-book reader comes with a 6-inch E Ink display that offers a resolution of 600 x 800 pixels meaning that it is fine for print, but images look like something out of a newspaper 30 years ago.
That screen dominates the proceedings. It's clear, grey and not backlit. Navigation controls are via a d-pad on the front underneath the screen or a series of buttons hidden on the side out of sight.
There is an SD card slot so you can expand on the 512MB of in-built memory included and to get books to and from the device it is merely a case of connecting it to a PC or Mac via a USB cable and dragging them across.
There is MP3 support for audio books or music while you read, although the Cybook Gen3 uses a 2.5mm, rather than 3.5mm, socket. It's annoying as chances are you don't have a 2.5mm jack floating around your house and this means another trip to the shops as there isn't one in the box.
MP3 playback is simple but ample - when was the last time a book, that wasn't aimed at under-5s, played you music?
So there are the tech specs, what of the experience?
Not wanting to come at this completely from a gadget side of things we hunted out an expert, a rare book dealer, to ask him what he thought of the e-book reader.
His opinion? Mixed.
While he liked the ability to change the font size and typeface to suit your reading style (handy if you've lost/forgotten your glasses) the non-tactile approach left him disappointed.
"At the end of the day, the device is simply feeding you text - albeit in a friendly way - and provides little of the 'touchy-feely' experience you get from a book - dog-eared pages, colourful artwork and that cream background."
In our tests we would have to agree. The Cybook Gen3 lacks basic elements that make a book a book. Due to the ability to resize and choose your font (you can add more beyond the three that come as standard) you don't get page numbers unless it's a PDF file, but instead a bar at the bottom suggesting where you are. For us this meant you lose any sense of progression through the book, or any real understanding of where you were.
Then there is the grey uninspiring display, no fault of the Cybook but it's not really that compelling making everything, well, grey. You get used to it of course just like any new technology but it's not the same.
So is it a page turner? Well the Cybook Gen3 has its pros and cons just like any other gadget we review here at Pocket-lint, although it has the ability to carry around 10,000 books, you're unlikely to dip in and out of books the same way you do music.
What we did like was the fact that it is incredibly light and so carrying around a book like War and Peace or Lord of the Rings doesn't have to be a heavy-handed affair.
However the lack of page numbers, the lack of a tactile experience and the fact you can't use it on a plane during take off and landing means that for now the e-book isn't about to replace your paperback.
It will eventually, and as e-books go this isn't a bad effort, however the rare book dealer (perhaps he is just trying to protect his job) and I aren't ready to go digital just yet.
This product was kindly loaned to us by Pixmania.com


text:
Your search did not match any results.
We suggest you try the following to help find what you're looking for:
In the era of automated, targeted, personalised CX, CMOs, in cooperation with IT, can futureproof their brand by tackling data ethics and security.
Discover how CMOs can team up with IT to protect both data and brand.
Marketing leaders need a consistent data strategy that will enable insights instantly, anyplace, anytime.
Find out how AI can have a massive impact on personalised, cross-channel marketing.
Find out how transparency and the ethical usage of customer data is central to marketing success.
Discover how Kenya Airways implemented AI technologies to deliver targeted, automated, and personal CX for marketing success.
Watch Sarah Speake from Speake Up Consulting talk about the happy marriage of marketing and IT.
In this episode, IDC and Oracle experts address ethical usage of data to build brand trust.
Find out more about intelligent automation for marketing success.


text:
MIT's Gediminas Urbonas emerged from the old Soviet Union to produce new art in Cambridge.December 19, 2012
World's first real-time digital computer and electronic navigation system are commemorated in Boston.June 28, 2012
President Susan Hockfield speaks on the struggle for America's future — then and now.February 9, 2012
Humanities, arts and social sciences digest for June 2011June 26, 2011
See the five-day process that started at Montilio's bakery in Brockton ended with the MIT150 sesquicentennial cake — all 750 pounds of it — being devoured at Toast to Tech.June 9, 2011
Tech Reunions 2011 brought a record number of participants to campus, drawn in part by the sesquicentennial celebrations. Reunion giving hit a new record.June 7, 2011
How a Swedish bon vivant let MIT introduce modern meteorology to America — just in time to help the Allies win World War II.June 7, 2011
Toast to Tech brings together the Institute community to cap its 150th anniversary celebrations in style.June 6, 2011
At MIT's 145th Commencement, Xerox chair Ursula Burns urges graduates to live so that they leave behind more than they take away.June 3, 2011
MIT Medical contest winner walks 12 miles during MIT open house on April 30June 2, 2011
Astronaut alumni wish MIT a happy 150th from 200 miles above.June 1, 2011
Friday's 145th Commencement exercises will celebrate MIT tradition.June 1, 2011
A letter written by Charles Stark Draper in 1961 hitches a ride on Space Shuttle Endeavour.May 31, 2011
Recognition Day honors laboratory's contributions to the nationMay 25, 2011
Institute community invited to the final anniversary celebration.May 25, 2011
Senate resolution cites 'the commitment of MIT to innovation and the entrepreneurial spirit.'May 24, 2011
Special Boston Globe magazine on MIT at 150 published Sunday; search-engine giant and U.K. newspaper post pieces about the Institute's impactMay 18, 2011
Thousands descend on campus for FAST Light, the finale of the Festival of Art + Science + Technology.May 9, 2011
Final installment of MIT's 150th anniversary symposia explores intelligence — both human and artificial.May 9, 2011
Online registration now open; guest services volunteers are vital to the event's success.May 4, 2011


text:
If you're unemployed, you perhaps have ample time in your day to search for a job. For others, landing a job is a time-sensitive matter; it's important to work quickly.
To make the best use of your time, follow these 10 tips to help you be more strategic in your job search:
1. Don't Apply for Everything
Sure, showering online application systems with your resume is pretty easy, and something should catch eventually, right? Maybe…the issue with indiscriminately applying to jobs, however, is that you really are wasting your time on opportunities that won't come to fruition, as well as wasting the time of the hiring manager who is scanning applications. What you should be doing is focusing on applying to jobs that you are qualified for, and putting together more thoughtful applications for these.
2. Don't Get Attached to One Particular Job
On the flip side, it's also important not to get too attached to one position in particular. You may think you have found your dream job, and therefore begin devoting all of your time and attention toward putting together your materials for it. But if it doesn't pan out you'll be stuck behind on everything else. Don't risk falling under the spell of one incredible job – spend a little extra time on your application and preparation for this particular position, but don't let the rest of your job search fall by the wayside.
3. Don't Constantly Re-Write Your Cover Letter
While it's important not to send a generic cover letter out to companies you are applying to, you also shouldn't waste your time crafting a new letter for each and every position you're interested in. Instead, create a few good templates that only require you to change a paragraph or so for each job.
4. Don't Constantly Revise Your Resume
Again, it's a waste of time to switch your resume around for each job prospect that presents itself. Here, too, it's helpful to save a few different copies that you can choose from, instead of carefully scrutinizing and tweaking your CV every single time.
5. Don't Get Sidetracked on the Internet
The problem with searching for jobs online, especially when you are networking on sites like LinkedIn or Facebook, is that you can so easily get distracted. Set ground rules for yourself and consider setting up a special email account for your career search so that personal emails don't sidetrack you.
6. Don't Apply to Every Job Available
Some people think that they're best chance at getting a job is to apply to every job they find online…literally every job, whether they are remotely qualified or not. It may seem like playing the numbers is a good bet, but in reality, trying to carpet bomb the internet with your resume won't result in any interviews.
7. Don't Stand Inline at a Job Fair
While some types of job fairs, like company specific or college job fairs can be worthwhile, you should avoid the mega-job-fairs typically held in arena, event or conference centers. In situations like these, you'll spend so much time traveling and waiting in line, its simply not worth the time.
8. Don't Pay a Headhunter
Real headhunters are paid by companies to fill positions. Unfortunately there are many former or want-to-be headhunters that can't find work with companies, and instead advertise their services to individuals. These people don't have access to any jobs you couldn't find yourself.
9. Don't Get Useless Certifications
Some people think if they get an obscure certification, it will make them look unique to employers. Unfortunately most employers don't care about your certifications if they aren't relevant to the job, even if you think they give you some special insight or advantage.
10. Don't Use Only Free Job Boards
Free job boards are open to anyone on the internet, and the jobs that are posted there often get a huge volume of resumes, many unqualified. For this reason, many employers choose to use subscription based job boards, because the candidate quality is so much better. Don't miss out on these jobs in the hidden job market. Try using a paid job board like Doostang.com, and see how much better the job quality is.
Unfortunately, there is a myriad of ways to get distracted and waste time in the search for your next job. Just remember how important your time and ability to focus are, and try to avoid the above productivity drains.
For this post, YouTern thanks our friends at Doostang!
Founded in 2005 at Harvard, Stanford and MIT, Doostang was created with one goal in mind: to successfully advance ambitious young professionals in their careers. Doostang offers its members the opportunity to search thousands of high-quality, highly relevant job opportunities, and tools to leverage their inside connection to get hired. Follow Doostang on Twitter!


text:
FREE SHIPPING on Orders Over $49! | Easy Returns & No Restocking Fee!
Get help from Customer Care
(800) 357-5044
Chat Live
Contact Us
Track Order -
Returns -
Shipping Info
If your are new user, Sign Up Here
Already have an account? Sign in here
with Special Savings, Discounts & New Products!
Contact Us


text:
Marburg Institute Photographs Collection
- Marburg MSS
- Coleção
- c.1930s
15 black and white photographs of well-known monuments. Photographs made for the project 'Sondermappe Bilder zur aegyptischen Kunst'.
Marburg Institute
27 resultados com objetos digitais Mostrar resultados com objetos digitais
Marburg Institute Photographs Collection
15 black and white photographs of well-known monuments. Photographs made for the project 'Sondermappe Bilder zur aegyptischen Kunst'.
Marburg Institute
Margaret Alice Murray Collection
Notes collected on Hierakonpolis (The Hierakonpolis finds). Consists of handwritten notes made by M. A. Murray, typescript, and additional notes in a different hand.
Murray, Margaret Alice
Metropolitan Museum of Art Photographs Collection
Two incomplete sets of Series T photographs of private tombs at Thebes, in addition some negatives of the same. Incomplete set of photographs of royal tombs in the Valley of the Kings. Photographs of the tomb of Nefertari (QV 66). Incomplete set of photographs of the Temple of Hatshepsut at Deir el-Bahri.
Metropolitan Museum of Art, New York
Photographs of foreigners as represented on various Egyptian monuments.
Meyer, Eduard
Diary kept from 4 May 1922 to 20 October 1926 by the wife of the British archaeologist and photographer Harry Burton (1879-1940). The diary contains detailed daily entries recording social engagements and memorable events, including the excavation of the tomb of Tutankhamun by Howard Carter's team, of which her husband was a member. The diary details her life and travels with her husband at home in Florence, their stays in Egypt (especially Luxor, but also Cairo), the trip they made across the US and to Hollywood in 1924, and various holidays in Europe (London, Salzburg, St. Moritz, etc.), as well as trips to friends in Italy. Lined account book, 400 pages, 8vo (179 x 110 x 28 mm).
Burton, Minnie Catherine
Complete papers.
Gilula, Mordechai
Myrtle Florence Broome Collection
415 items of correspondence written by Miss Broome to her parents whilst working at Abydos between 1927 and 1937.
Fifteen items are groups of two letters (16, 35, 51, 55, 97, 111, 154, 198, 227, 268, 319, 325, 363, 408, and 414, not all of them by Miss Broome), three of which are actually postcards (16A and 414A-B); item 156 is a group of three letters [= 429 letters and 3 postcards in total].
A few letters include drawings/maps; seven letters include photographs (111, 123, 273-276, and 279); letter 337 includes a newspaper cutting; some other letters mention the enclosure of additional items which are now lost.
Broome, Myrtle Florence
Norman de Garis and Nina Davies Collection
Papers, including notebooks, notes, tracings and squeezes, made in Theban tombs and elsewhere, photographs, collection of coloured hieroglyphic signs, indexes of scenes in Theban tombs, etc.
Davies, Norman de Garis
Oliver Robert Gurney Collection
Correspondence and notes relating to the geography of the Hittite Empire, Babylonian music, decipherment, and various other topics.
Gurney, Oliver Robert
Osbert Guy Stanhope Crawford Collection
Maps, plans and drawings.
Crawford, Osbert Guy Stanhope
Notebook containing the transcription and notes on papyrus Reisner I.
Smither, Paul Cecil
Card indexes, photographs, notebooks, notes, copies, correspondence, typescripts, and negatives.
Kahle, Paul Eric
Material (mostly photographic) on the Luristan bronzes. It appears to relate to a planned joint publication with Frank Savery, paid by the Griffith Institute. The material was eventually published by Roger Moorey. Non-Egyptological.
Jacobsthal, Paul
Percy Edward Newberry Collection
The Percy Newberry Collection has been listed thanks to a cataloguing grant from the The National Archives in 2015. The collection comprises a wide range of material on topics including Predynastic Egypt, Theban tombs, Egyptian flora and fauna, early Egyptian travellers, ancient Egyptian religion and culture, as well as Newberry's genealogy. Formats include notebooks, research notes, photographs, tracings, rubbings and neswpaper clippings.
The collection has been divided into 5 series: Biographical Material; Correspondence; Research Notebooks; Subject Files and Research Material.
The following key subject terms collate material on the same subject which have been listed in different series:
Nome Ensigns
Flora and Fauna
Predynastic Egypt
Scarabs and Seals
Newberry, Percy Edward
Peter Le Page Renouf Collection
Renouf, (Sir) Peter Le Page
Peter Webb and Ron Davey Collection
Notes, colour transparencies and photographs of shabtis, monuments and other objects.
Webb, Peter
Philipp Remelé Photographs Collection
21 photographs. 13 of the Temple of Hibis at el-Khârga Oasis, and 8 of the Temple of Deir el-Hagar at el-Dâkhla Oasis.
Remelé, Philipp
Bound manuscript on Egyptian hieroglyphs and related topics (Roman obelisks, Iseum in Rome, Isiac pomp described by Apuleius, Egyptian rites, mummies, etc.). Left unfinished.
Bracci, Pietro
Site indexes to the Journal d'Entrée and Temporary registers of the Egyptian Museum, Cairo.
Engelbach, Reginald
Three A4 folders containing an unpublished annotated typescript of a monograph on the constellations of the Babylonian and Egyptian sphere and their modifications by the Greeks of the Achaean period.
Eisler, Robert
Robert Elcum Horsfall Negatives Collection
Negatives of Egyptian sites and monuments taken before 1914.
Horsfall, (Capt) Robert Elcum
Typescript copy of Hay's journal from 24th November 1824 to 27th October 1827, photographs of drawings made by Hay in the tomb of Neferhotp (TT49) (Griffith Institute photos. 3070-7), 13 mounted photographs made from Hay's drawings of el-Kâb, Philae, and Amada, and microfilm roll with copies of the Hay MSS once in the British Museum and now in the British Library.
Hay, Robert
Prints and negatives of scenes in Theban tombs, notebook and notes (some by W. B. Emery and E. J. H. MacKay).
Mond, (Sir) Robert Ludwig
Robert McLachlan Wilson Collection
Copies, notes, transcripts, photographs, and correspondence relating to the surviving fragments of the New Testament in the Faiyumic dialect of Coptic. Continuing the work of P. E. Kahle, see Kahle MSS 2/13 New Testament Faiyumic Texts.
Includes correspondence from:
-Paul Eric Kahle, 1959
-Elinor Husselman (Kelsey Museum of Archaeology, University of Michigan), 1959-1961
-Walter Till (Department of Coptic Studies, University of Manchester), 1958-1959
-Theodore Petersen (St Paul's College, Washington), 1965
-R. Kasser (Professor of Coptic language and literature, University of Geneva), 1987
Wilson, Robert (Robin) McLachlan
Robert Thomas Rundle Clark Collection
Notes, notebooks, some correspondence, annotated offprints, lantern slides and a small number of photographs and negatives.
Clark, Robert Thomas Rundle
Robert Walter Sloley Collection
Various notes.
Sloley, Robert Walter
Rosalind Frances Emily Paget Collection
Coloured drawings of hieroglyphs.
Paget, Rosalind Frances Emily
Rudolph Theophilus and Alice Lieder Squeezes Collection
Paper squeezes of monuments made in Egypt in 1850-3.
Lieder, (Revd Johann) Rudolph Theophilus
One notebook.
Birch, Samuel
Sarah Joanne Clackson Collection
Notes, transcriptions, translations, article drafts, lecture drafts, card index, photographs, slides, overhead projector sheets, electronic data files, microfilm, correspondence, annotated photocopies and off-prints, relating to Coptic and Greek documents and Coptic archaeology.
Clackson, Sarah Joanne


text:
This story appears in the January 2013 issue of National Geographic magazine.
On the edge of a parking lot at the Marshall Space Flight Center in Huntsville, Alabama, stands a relic from a time when our future as a spacefaring species looked all but inevitable, as clear and grand as a rocket ascending over Cape Canaveral.
"This is not a model," NASA physicist Les Johnson says as we gaze at the 35-foot-tall assemblage of pipes, nozzles, and shielding. "This is an honest-to-goodness nuclear rocket engine." Once upon a time, NASA proposed to send a dozen astronauts to Mars in two spaceships, each powered by three of these engines. Marshall director Wernher von Braun presented that plan in August 1969, just two weeks after his Saturn V rocket delivered the first astronauts to the moon. He suggested November 12, 1981, as a departure date for Mars. The nuclear engines had already passed every test on the ground. They were ready to fly.
Thirty years after the Mars landing that never was, on a humid June morning, Johnson looks wistfully at the 40,000-pound engine in front of us. He heads a small team that assesses the feasibility of "advanced concepts" in space technology—and NERVA, the old nuclear engine, just might qualify. "If we're going to send people to Mars, this should be considered again," Johnson says. "You would only need half the propellant of a conventional rocket." NASA is now designing a conventional rocket to replace the Saturn V, which was retired in 1973, not long after the last manned moon landing. It hasn't decided where the new rocket will go. The NERVA project ended in 1973 too, without a flight test. Since then, during the space shuttle era, humans haven't ventured more than 400 miles from Earth.
All of which might seem to make the question Johnson and I have spent the morning discussing—will humans ever travel to the stars?—sound a little out of touch.
Why did it seem more reasonable half a century ago? "Of course we were crazy in a way," says physicist Freeman Dyson of the Institute for Advanced Study in Princeton. In the late 1950s Dyson worked on Project Orion, which aimed to build a manned spacecraft that could go to Mars and the moons of Saturn. Instead of using nuclear reactors to spew superheated hydrogen, as NERVA did, the Orion spacecraft would have dropped small nuclear bombs out the back every quarter of a second or so and surfed on the fireballs. "It would have been enormously risky," says Dyson, who planned to go to Saturn himself. "We were prepared for that. The mood then was totally different. The idea of a risk-free adventure just didn't make sense." A few years after Orion ended, Dyson outlined in Physics Today how a bomb-powered spacecraft might travel to a star.
These days it's easier to outline why we'll never go. Stars are too far away; we don't have the money. The reasons why we might go anyway are less obvious—but they're getting stronger. Astronomers have detected planets around many nearby stars; soon they're bound to find one that's Earthlike and in the sweet spot for life, and in that instant they'll create a compelling destination. Our technology too is far more capable than it was in the 1960s; atom bombs aren't cutting-edge anymore. In his office that morning, Les Johnson handed me what looked like a woven swatch of cobwebs. It was actually a carbon-fiber fabric sample for a giant spaceship sail—one that might carry a probe beyond Pluto on rays of sunlight or laser beams. "Be very careful with it," Johnson said. "This is a material that might help us get there."
To get to the stars, we'll need many new materials and engines but also a few of the old intangibles. They haven't vanished. In fact, they almost seem to be bursting forth again in the imaginative space vacated by the space shuttle, which in 2011 joined the Saturn V as a museum exhibit. In the conversation of certain dreamer-nerds, especially outside NASA, you can now hear echoes of the old aspiration and adventurousness—of the old craziness for space.
Last spring, three weeks before I met with Johnson, SpaceX, a private company based near Los Angeles, used one of its own rockets to launch an unmanned capsule that docked with the International Space Station. SpaceX leads several other companies in the race to replace the shuttle as the space station's supply ship. A month before that, a company called Planetary Resources, backed by billionaire investors such as Google's Larry Page and Eric Schmidt, announced plans to use robotic spacecraft to mine asteroids for precious metals. Working with Virgin Galactic, a company whose main business is space tourism, Planetary Resources expects within the next year or two to launch a lightweight telescope into low Earth orbit. "We hope by the end of the decade that we will have identified our initial targets and begun prospecting," says Peter Diamandis, the firm's co-founder.
"We're going to look back at this decade as the dawn of the commercial space age," says Mason Peck, NASA's chief technologist. "It's about companies large and small finding ways to make a market out of space. The energy we see now—the economic motivation to go into space—we haven't seen that before."
Economics has long spurred exploration on Earth. Medieval merchants risked the hazards of the Silk Road to reach the markets of China; Portuguese caravels in the 15th century sailed beyond the bounds of the known world, searching less for knowledge than for gold and spices. "Historically, the driver for opening frontiers has always been the search for resources," says Diamandis. "Science and curiosity are weak drivers compared with wealth generation. The only way to really open up space is to create an economic engine, and that engine is resource extraction."
One resource he and co-founder Eric Anderson have their eyes on is platinum, so rare on Earth that it currently fetches $1,600 an ounce. Sending robots a million miles or more to extract and refine ore on asteroids in near-zero gravity, or to tow an asteroid closer to Earth, will require technology that doesn't yet exist. "There's a significant probability that we may fail," Anderson said at the press conference in April. "But we believe that attempting this and moving the needle for space is important. Of course we hope to make a lot of money."
Elon Musk, the 41-year-old founder of PayPal, Tesla Motors, and SpaceX, has already made a lot of money, and he is devoting a sizable portion of that fortune to his own space program. The new rocket SpaceX is developing, the Falcon Heavy, will be capable of carrying twice the payload of the space shuttle, he says, for about one-fifth the price. His goal is to reduce launch costs by a further factor of 50 or 100, to $10 to $20 a pound, by developing the first fully reusable rockets. "This is extremely difficult, and most people think it's impossible, but I do not," Musk says. "If airplanes had to be thrown away after every flight, no one would fly."
For Musk, it's all part of a much grander plan: establishing a permanent human colony on Mars. NASA has had enormous success on Mars with unmanned rovers, most recently Curiosity, but has repeatedly pushed back a manned mission. Musk thinks SpaceX could land astronauts on Mars within 20 years—and then keep landing them for decades after that.
"The real thing that's needed is not to send one little mission to Mars," he says. "It's ultimately to take millions of people and millions of tons of equipment to Mars to make it a self-sustaining civilization. It will be the hardest thing humanity has ever done, and it's far from certain that it will occur.
"I should emphasize this is not about escaping Earth. It's about making life multiplanetary. It's about getting out there and exploring the stars."
The fastest spacecraft ever built—the Helios 2 probe, launched in 1976 to monitor the sun—attained a top speed of 157,000 miles an hour. At that rate, a spacecraft headed to Proxima Centauri, the nearest star, would take more than 17,000 years to make the 24-trillion-mile journey, a temporal span equal to the one that separates us from Cro-Magnon cave painters. Those inescapable facts lead even some of the staunchest advocates of human spaceflight to conclude that interstellar travel, aside from robotic probes, will remain forever in the realm of science fiction. "It's Mars or nowhere," says Louis Friedman, an astronautics engineer and one of the founders of the Planetary Society, a space-exploration advocacy group.
Some scientists, however, find the prospect of eternal confinement to two small planets in a vast galaxy just too depressing to contemplate. "If we start now, and we have started, I believe we can achieve some form of interstellar exploration within a hundred years," says Andreas Tziolas. A physicist and former NASA researcher, Tziolas is a leader of Icarus Interstellar, a nonprofit organization that aims, as its mission statement says, "to realize interstellar flight before the year 2100." It is now collaborating with former shuttle astronaut Mae Jemison. In early 2012 the Defense Advanced Research Projects Agency (DARPA) awarded her $500,000 for something called the 100 Year Starship project. "Our task is not to launch a starship but to make sure the technologies and abilities exist within the next hundred years to do that," Jemison says.
Tziolas thinks we could develop a starship engine that harnesses nuclear fusion, the energy source of stars and hydrogen bombs. When the nuclei of small atoms such as hydrogen fuse, they release enormous energy—much more than is released by the nuclear fission of large atoms such as uranium, the energy source of nuclear power plants and of the old NERVA. While physicists have built fusion reactors, they haven't yet found a way to make one that yields more energy than it consumes. "I have faith in our ingenuity," Tziolas says. Only seven decades elapsed between the discovery of subatomic particles and NERVA, he points out; by 2100, he thinks, we should be able to create a fusion engine that could propel a starship to a top speed of 15 to 20 percent of the speed of light.
That would allow it to reach the nearest star in another few decades—if its machinery could last that long. "Twenty years is getting near the upper limit for how long you can design a spacecraft to reliably operate," says Les Johnson. NASA asked Johnson to look into a 20-year mission, not to a star but to the edge of interstellar space—to the region known as the heliopause, several times as far as Pluto, where the sun's influence is balanced by that of other stars. "The thought was, you don't want to immediately start talking about going to the nearest star," says Johnson. "It's over four light-years away. It's just ... daunting, unfathomable." Johnson's task was to plan a realistic mission with a technology that's at least close to existing—a first small step toward the stars.
Right now, fusion engines aren't close to existing; a nuclear engine like NERVA would be too expensive; chemical rockets might reach the heliopause but could never carry enough fuel to reach a star in a reasonable amount of time. (The Voyager spacecraft, were it headed the right way, would drift by Proxima Centauri in 74,000 years.) In the end Johnson's team settled on the most evocative technology: a solar sail. Sunlight, like all light, consists of particles called photons, which exert pressure on everything they touch. At Earth's distance from the sun, the pressure is only about a tenth of an ounce spread over a football field. But a large, thin sheet of reflective fabric, unfurled in the vacuum of space, will feel this gentle force and will slowly accelerate.
NASA launched a 110-square-foot light sail in 2010 that survived for several months in low Earth orbit. It hopes to launch a sail in 2014 that measures a bit under a third of an acre and weighs just 70 pounds. Movable vanes on the corners will allow ground control to maneuver the Sunjammer, which on its yearlong mission will tack some two million miles upwind toward the sun. A 16-billion-mile mission to the heliopause would require a disk-shaped sail 1,500 feet in diameter. After a year or two of sailing, the spacecraft would exceed 100,000 miles an hour.
Proxima Centauri lies 1,500 times farther still. "To sail to another star," Johnson says, "we'll need a sail the size of Alabama and Mississippi combined. We don't know how to build that yet." What's more, sunlight alone couldn't push the sail to the star within a human lifetime, or even many lifetimes; you'd need powerful space-based lasers. "If you take the total energy output of humanity and put it in a laser on a satellite," says Johnson, "then you could get trip times of a few decades to Proxima Centauri." And that's to send a robot the size of Johnson's desk.
What about humans, with their need for 24/7 life support? Johnson throws up his hands. "When you start thinking about what it takes to supply people," he says, "and how big the spacecraft would have to be and how much energy it would have to have, you enter the realm of science fiction."
To build a starship, you first have to build a future that converts fiction into fact, and that takes a lot more than rocket science. The task isn't figuring out right now how to design a starship; it's continuing to build the civilization that will one day build a starship. Framed like that, more expansively, it begins to seem less impossible. But it's a 100-year project or maybe a 500-year project, depending on your craziness level. Johnson's level is lowish.
"I don't know what the world will be like in 500 years," he says. "If we have fusion power plants, and space-based solar panels beaming energy down, and we're mining the moon and have an industrial base in low Earth orbit—maybe a civilization like that could do it. We'll have to be a civilization that spans the solar system before we can think about taking an interstellar voyage."


text:
So here let me focus on NAS signally aspects of LTE. It is highly preferable to have some prior knowledge about any wireless technology : 2G, 3G or 4G. This LTE-NAS series will provide some idea about LTE basic procedures and signaling message exchanges. They are called NAS messages. One can always refer 3GPP standard to learn NAS. But here I wrote it differently, in my own wordings, at my blog 'Express YourSelf !' Enjoy it and let me know your feedback.
Even UMTS has NAS. NAS messages are for (1) Mobility (2) Session Management and (3) Security. Security has two aspects: (1)integrity and (2)ciphering. Today's article is about EMM. EMM includes determining UE's location, user's authentication, confidentiality, and connection management. Procedure is a group of NAS messages exchange with specific purpose. There are two kinds of EMM elementary procedures. (1) Common procedures and (2) specific procedures.
Let's see specific procedures, (1)Attach, (2)Detach and (3) TAU are EMM's specific procedures. As the name suggest, UE invokes attach procedure to attach to LTE network and to detach from LTE network, the detach procedure. These procedures are invoked when UE is powered ON (attach) or OFF (detach). Also when UE enters to LTE coverage area (attach) or leave LTE coverage area (detach). Simple to understand. Is not it? Generally UE and network both are backward compatible. So UE may perform combined attach/detach for (1) new LTE network and (2) legacy GPRS/UMTS network. To support such combine procedure is optional. Normal attach and combined attach are differ only by presence of few optional IEs. There are three kinds of UEs. PS only mode UE works only with EPS (EPS is synonymous for LTE). These UEs are not mobile handsets but they are USB dongle or PC card. They never perform combined procedure. "CS/PS mode 1 UE" and "CS/PS mode 2 UE" are dual mode. If UE is under coverage of both LTE and legacy GPRS/UMTS, then Mode 1 UE prefers non-EPS (GPRS/UMTS) and mode 2 prefers EPS(LTE) service. However, they can attach to both networks, (1) EPS network and (2) non-EPS network.
What is TAU? TA is formed by coverage are of a group of cell sites (eNBs). LA in 2G GSM, RA in GPRS. eNB broadcasts TAI. When the moving UE change its TA, it informs the network about its new TA or TA list with "normal TAU procedure". Even if UE is stationary, it periodically reports its TA with "periodic TAU procedure". Our 2G GSM MS perform LAU at about every 3 hours. GPRS MS perform RAU at about every 50 to 55 minutes. TAU can also be combined TAU, to inform legacy GPRS/UMTS network, with help of eUTRAN LTE infrastructure. So if network supports combine procedures, then dual mode UEs can perform combine procedure. The combined procedures save UE's battery power and network's scare radio resources. :)
After knowing the purpose of EMM procedure, let's have closer look to them. The EMM Specific procedures in turn may optionally invoke common procedures. For example, EMM specific procedure named Attach may invoke other EMM common procedure(s) like (1)GUTI relocation, (2)Authentication, (3)Security Mode control, (4)Identification, (5)EMM Information and (6)ESM Information. They are optional. The common procedures and specific procedures, both are EMM elementary procedure. Let me describe this concept with a class diagram !!
Yes, I know, we use UML class diagram for design a software module. Here I have used just to make the point clear. It is not for design of NAS module neither at UE nor at MME.
Have you noticed? I used italic fonts in diagram to indicate abstract class They are still category only, not any concrete procedure. Here all EMM Specific procedures and few ECM specific procedures may optionally invoke EMM common procedure(s). So these specific procedures are "whole", common procedure(s) are "part" and this is aggregation relationship. Also, if you observe carefully the class diagram looks like Composite design pattern.
RRC carries NAS messages. In UMTS, RRC is terminating at RNC. LTE network, does not have RNC so RRC is terminating at eNB. NAS terminates at MME. NAS messages are between UE and MME. RRC and NAS both provides data integrity. Ciphering is mandatory for RRC, but optional for NAS. NAS can have at least two FSMs for (1) ESM FSM and (2) EMM FSM. EMM FSM has seven states. (1) EMM Null, (2) EMM DeRegistered, (3) EMM DeRegistered initiated, (4) EMM Registered, (5) EMM Registered initiated, (6) EMM TAU initiated, (7) EMM Service Request initiated. Have you noticed? Out of these seven states, most of them are transient states. EMM FSM has major two states only. EMM DeRegistered and EMM Registered. They are correspond to UE is power OFF and UE power ON (with valid subscription :-) ) respectively. ECM can have its FSM. For EMM Registered state, ECM FSM has two states. (1) ECM idle and (2) ECM connected. They are also known as EMM Idle and EMM Connected respectively.
Subsequent articles will cover more details about ECM, ESM and security etc...
2 comments:
- Anonymous said...
情色成人網站 -
情色成人論壇 -
18情色成人網 -
台灣18情色成人 -
情色成人圖片 -
情色成人聊天室 -
18禁情色成人影音 -
18情色成人 -
情色成人短片 -
卡通情色成人網 -
小瓢蟲情色成人動畫 -
情色成人娛樂 -
愛愛情色成人貼片區 -
69情色成人無碼 -
情色成人貼片 -
免費情色成人圖片 -
情色成人天下淫書 -
情色成人動畫 -
嘟嘟情色成人貼圖 -
免費下載情色成人短片 -
嘟嘟情色成人網站 -
十八禁情色成人卡漫 -
金瓶梅情色成人網 -
免費情色成人短片 -
情色成人哈啦聊天室 -
免費情色成人影片 -
台灣十八情色成人網 -
熊貓情色成人 -
情色成人自拍 -
情色成人小遊戲 -
台灣情色成人貼圖 -
情色成人黃色笑話 -
小弟弟情色成人娛樂網 -
免費情色成人小說 -
情色成人文章 -
情色成人18禁 -
免費18禁情色成人圖片 -
情色成人聊天 -
- December 11, 2009 at 12:46 PM
- Manish Panchmatia said...
Hi all
Please have a look to this complete white paper about "LTE NAS Procedure" http://layers7.blogspot.in/2012/09/lte-nas.html
-Manish V. Panchmatia
- September 18, 2012 at 12:27 AM


text:
Relive This Year's Easter on the Bayou with These Great Photos
What looked to be the start of a dreary day for Easter on the Bayou turned out to be a great day full of fun. There were many colorful, candy-filled eggs scattered throughout the woods for the children to hunt, good food and other fun activities for the families to enjoy.
The gates opened about 8 a.m. and the Easter egg hunting and activities began at 10. Children enjoyed bouncy houses, inflatable slides, face painting booths and an inflatable rock climbing wall. Vendors such as McAlister's and Newk's Restaurants, as well as the event sponsor, MetroPCS, had booths set up down by the picnic area where some families enjoyed lunch down by the water. Overall, a good time was had by all.
We captured plenty of photos during Easter on the Bayou, so be sure to check them out to see if you recognize anyone! Happy Easter!


text:
The Apex Police Department is equipped with a 24 hour Emergency Communications Center with trained and certified Telecommunicators that answer both 911 phone lines and non- emergency administrative phone lines. Telecommunicators are a vital link to Police officers, firefighters and EMS workers within Apex and surrounding area. Telecommunicators are the first public contact many people have when assistance is needed.
The center is equipped with the latest technology in order to maintain the Town's commitment to quality service. The main components include Enhanced 911, Computer Aided Dispatch, and Telecommunications Device for the Deaf (TDD).
In addition to 911 Emergency Services and Communications, we are the primary after hours contact for answering requests for service for the Town of Apex utilities and for dispatching Town of Apex utility workers.
The professional staff of the Communications Division is dedicated to providing quality service to the citizens and first responders.


text:
Check Out This Awesome, Fan-Made 'Jurassic Park' Computer-System Re-creation
There's nothing too nerdy for us when it comes to movies – in fact, the more nerdy and obscure something movie related is, the more likely we are to love it. Take, for instance, this awesome time waster that pays homage to one of the lesser unforgettable scenes in Steven Spielberg's Jurassic Park.
Remember how things all went wrong in the film? Hacker Dennis Nedry decides he's not above taking a payoff to steal Dinosaur DNA and get it off the island for a huge payday. To facilitate his thievery, Nedry hacks the security system and makes it so no one can override what he's done. Samuel L. Jackson's Ray Arnold gives it his best shot, but his efforts come up short. After three failures, he's taunted by an image of Nedry's head on an Elvis body repeatedly telling him he "didn't say the magic word…"
Leave it to the Internet to re-create the entire computer interface of that scene just so you too can feel Arnold's frustration. Heading over to Jurassic Systems will allow you to play around in an HTML5/Javascript re-creation of the computer systems in the film.
After watching a video of the scene from Jurassic Park, users will be free to enter their own commands into the interface. After three fails, you get to see Nedry firsthand. It's a pretty neat way to kill a few minutes, plus there's apparently at least one hidden command according to the creators. I couldn't find it, but if you've got the time, maybe you can. Just resist the urge to punch your monitor after Nedry taunts you repeatedly for your failings.
Follow @Horrorgeek Follow @MoviesDotCom
Movies.com, the ultimate source for everything movies, is your destination for new movie trailers, reviews, photos, times, tickets + more! Stay in the know with the latest movie news and cast interviews at Movies.com.
Copyright © 2020 FANDANGO MOVIES.


text:
This forum has some custom tags across the top, including a tag that links to what most of us consider our "parent forum", Giant in the Playground.
We're a rather straightforward place with a simple set of rules: don't be a dick. You can curse, you can argue, you can even talk about topics for your homebrew that aren't generally considered allowed topics for many other forums. But if the administration (there's a couple of us: our names are in red) finds that you're being a jerk, or are trolling, or are even just spamming links to porn or whatever, you'll get warned, your post will be edited, and if you are enough of a repeat offender, you'll get banned. But, let's be fair: every forum has some sort of rules, so this should be nothing new.
We do have plans in the future to set up a program wherein you can publish your material through Competitor, using it as your publishing label. Of course we'll have a screening process so we can keep a high quality standard, but we'll also attempt to help you get your creations up to that standard. That is actually one of the things that the founders pride themselves on: I, and my associates, strongly feel that the greatest strength of pen and paper games is their infinite expandability, and the best way to do that is to assist others in making their creations the best that they can be.
So, once again, welcome to Competitor Games! Happy homebrewing!
--James Raine