Copyright | (c) 2018--2020 Michael Walker |
---|---|

License | MIT |

Maintainer | Michael Walker <mike@barrucadu.co.uk> |

Stability | experimental |

Portability | BangPatterns, FlexibleContexts, LambdaCase, RankNTypes |

Safe Haskell | None |

Language | Haskell2010 |

Internal types and functions for SCT. This module is NOT considered to form part of the public interface of this library.

## Synopsis

- sct :: (MonadDejaFu n, HasCallStack) => Settings n a -> ([ThreadId] -> s) -> (s -> Maybe t) -> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace))) -> Program pty n a -> n [(Either Condition a, Trace)]
- sct' :: (MonadDejaFu n, HasCallStack) => Settings n a -> ConcurrencyState -> s -> (s -> Maybe t) -> (s -> t -> n (s, Maybe (Either Condition a, Trace))) -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> ThreadId -> IORefId -> n [(Either Condition a, Trace)]
- simplifyExecution :: (MonadDejaFu n, HasCallStack) => Settings n a -> ConcurrencyState -> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> ThreadId -> IORefId -> Either Condition a -> Trace -> n (Either Condition a, Trace)
- replay :: MonadDejaFu n => (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) -> [(ThreadId, ThreadAction)] -> n (Either Condition a, [(ThreadId, ThreadAction)], Trace)
- simplify :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- lexicoNormalForm :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- permuteBy :: Bool -> MemType -> ConcurrencyState -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- dropCommits :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- pullBack :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- pushForward :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- renumber :: MemType -> Int -> Int -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)]
- toId :: Coercible Id a => Int -> a
- fromId :: Coercible a Id => a -> Int

# Exploration

:: (MonadDejaFu n, HasCallStack) | |

=> Settings n a | The SCT settings ( |

-> ([ThreadId] -> s) | Initial state |

-> (s -> Maybe t) | State predicate |

-> (ConcurrencyState -> (Scheduler g -> g -> n (Either Condition a, g, Trace)) -> s -> t -> n (s, Maybe (Either Condition a, Trace))) | Run the computation and update the state |

-> Program pty n a | |

-> n [(Either Condition a, Trace)] |

General-purpose SCT function.

:: (MonadDejaFu n, HasCallStack) | |

=> Settings n a | The SCT settings ( |

-> ConcurrencyState | The initial concurrency state |

-> s | Initial state |

-> (s -> Maybe t) | State predicate |

-> (s -> t -> n (s, Maybe (Either Condition a, Trace))) | Run the computation and update the state |

-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Just run the computation |

-> ThreadId | The first available |

-> IORefId | The first available |

-> n [(Either Condition a, Trace)] |

Like `sct`

but given a function to run the computation.

:: (MonadDejaFu n, HasCallStack) | |

=> Settings n a | The SCT settings ( |

-> ConcurrencyState | The initial concurrency state |

-> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Just run the computation |

-> ThreadId | The first available |

-> IORefId | The first available |

-> Either Condition a | The expected result |

-> Trace | |

-> n (Either Condition a, Trace) |

Given a result and a trace, produce a more minimal trace.

In principle, simplification is semantics preserving and can be done without needing to execute the computation again. However, there are two good reasons to do so:

- It's a sanity check that there are no bugs.
- It's easier to generate a reduced sequence of scheduling decisions and let dejafu generate the full trace, than to generate a reduced trace directly

Unlike shrinking in randomised property-testing tools like
QuickCheck or Hedgehog, we only run the test case *once*, at the
end, rather than after every simplification step.

:: MonadDejaFu n | |

=> (forall x. Scheduler x -> x -> n (Either Condition a, x, Trace)) | Run the computation |

-> [(ThreadId, ThreadAction)] | The reduced sequence of scheduling decisions |

-> n (Either Condition a, [(ThreadId, ThreadAction)], Trace) |

Replay an execution.

# Schedule simplification

simplify :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Simplify a trace by permuting adjacent independent actions to reduce context switching.

lexicoNormalForm :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Put a trace into lexicographic (by thread ID) normal form.

permuteBy :: Bool -> MemType -> ConcurrencyState -> [ThreadId -> ThreadId -> Bool] -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Swap adjacent independent actions in the trace if a predicate holds.

dropCommits :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Throw away commit actions which are followed by a memory barrier.

pullBack :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Attempt to reduce context switches by "pulling" thread actions back to a prior execution of that thread.

Simple example, say we have ```
[(tidA, act1), (tidB, act2), (tidA,
act3)]
```

, where `act2`

and `act3`

are independent. In this case
`pullBack`

will swap them, giving the sequence ```
[(tidA, act1),
(tidA, act3), (tidB, act2)]
```

. It works for arbitrary separations.

pushForward :: Bool -> MemType -> ConcurrencyState -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] Source #

Attempt to reduce context switches by "pushing" thread actions forward to a future execution of that thread.

This is kind of the opposite of `pullBack`

, but there are cases
where one applies but not the other.

Simple example, say we have ```
[(tidA, act1), (tidB, act2), (tidA,
act3)]
```

, where `act1`

and `act2`

are independent. In this case
`pushForward`

will swap them, giving the sequence ```
[(tidB, act2),
(tidA, act1), (tidA, act3)]
```

. It works for arbitrary separations.

:: MemType | The memory model determines how commit threads are numbered. |

-> Int | First free thread ID. |

-> Int | First free |

-> [(ThreadId, ThreadAction)] | |

-> [(ThreadId, ThreadAction)] |

Re-number threads and IORefs.

Permuting forks or newIORefs makes the existing numbering invalid, which then causes problems for scheduling. Just re-numbering threads isn't enough, as IORef IDs are used to determine commit thread IDs.

Renumbered things will not fix their names, so don't rely on those at all.