RE: type-checker plugin API/behaviour change

[Simon Peyton Jones via ghc-devs]

That looks plausible to me.

The ‘new’ bunch may not actually be new?   Maybe they are some of the inputs 
that are no contradictory, but not yet solved either?

What about a flag to say “I made some progress”?   Or is that deducible?  Is 
so, good to explain that.

Caveat: I’m not a user of plugins!  People who are should reply.

Simon

From: ghc-devs  On Behalf Of Christiaan Baaij
Sent: 18 July 2018 12:52
To: ghc-devs@haskell.org
Cc: Adam Gundry 
Subject: type-checker plugin API/behaviour change

Hi devs,

Currently, type-checker plugins get to tell the solver its progress using a 
[TcPluginResult](
http://hackage.haskell.org/package/ghc-8.4.1/docs/TcRnTypes.html#t:TcPluginResult):

```
data TcPluginResult
  = TcPluginContradiction [Ct]
-- ^ The plugin found a contradiction.
-- The returned constraints are removed from the inert set,
-- and recorded as insoluble.

  | TcPluginOk [(EvTerm,Ct)] [Ct]
-- ^ The first field is for constraints that were solved.
-- These are removed from the inert set,
-- and the evidence for them is recorded.
-- The second field contains new work, that should be processed by
-- the constraint solver.
```

So when asked to solve a _set_ of constraints, a tc plugin basically gets to 
say:

A) This _one_ constraint out of the entire set is wrong, or
B) The following _subset_ of constraints is solved (plus some new wanted 
constraints)

Supposedly, picking A leads to better error messages when a constraint is 
obviously bad (i.e. Int ~ Char). However, the issue is that when a tc plugin 
picks A, then it will not be called again for the whole set of constraint it 
originally got; which in my use-case basically leads to a complete set of 
(actually solvable) unsolved constraints.
This is "bad" because it leads to very confusing error messages, when

1. Start with a correct program: All constraints solvable => no errors reported
2. Add one line of code that doesn't type check
3. All constraints unsolvable => errors reported in parts of the program that 
used to type-check.

I thought of multiple possible solutions, but changing TcPluginResult to:

```
data TcPluginResult
  = TcPluginResult
  { contradictions :: [Ct]
  -- ^ All of the contradictions the plugin found
  , solved :: [(EvTerm,Ct)]
  -- ^ Constraints that were solved
  , new :: [Ct]
  -- ^ New work to be processed by the rest of the constraint solver
  }
```

seems the best one as it allows a tc plugin to report _all_ the constraints 
that are bad, and _all_ the constraints that are bad.

Thoughts? Perhaps a better solution?

Thanks,

Christiaan
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

type-checker plugin API/behaviour change

[Christiaan Baaij]

Hi devs,

Currently, type-checker plugins get to tell the solver its progress using a
[TcPluginResult](
http://hackage.haskell.org/package/ghc-8.4.1/docs/TcRnTypes.html#t:TcPluginResult
):

```
data TcPluginResult
  = TcPluginContradiction [Ct]
-- ^ The plugin found a contradiction.
-- The returned constraints are removed from the inert set,
-- and recorded as insoluble.

  | TcPluginOk [(EvTerm,Ct)] [Ct]
-- ^ The first field is for constraints that were solved.
-- These are removed from the inert set,
-- and the evidence for them is recorded.
-- The second field contains new work, that should be processed by
-- the constraint solver.
```

So when asked to solve a _set_ of constraints, a tc plugin basically gets
to say:

A) This _one_ constraint out of the entire set is wrong, or
B) The following _subset_ of constraints is solved (plus some new wanted
constraints)

Supposedly, picking A leads to better error messages when a constraint is
obviously bad (i.e. Int ~ Char). However, the issue is that when a tc
plugin picks A, then it will not be called again for the whole set of
constraint it originally got; which in my use-case basically leads to a
complete set of (actually solvable) unsolved constraints.
This is "bad" because it leads to very confusing error messages, when

1. Start with a correct program: All constraints solvable => no errors
reported
2. Add one line of code that doesn't type check
3. All constraints unsolvable => errors reported in parts of the program
that used to type-check.

I thought of multiple possible solutions, but changing TcPluginResult to:

```
data TcPluginResult
  = TcPluginResult
  { contradictions :: [Ct]
  -- ^ All of the contradictions the plugin found
  , solved :: [(EvTerm,Ct)]
  -- ^ Constraints that were solved
  , new :: [Ct]
  -- ^ New work to be processed by the rest of the constraint solver
  }
```

seems the best one as it allows a tc plugin to report _all_ the constraints
that are bad, and _all_ the constraints that are bad.

Thoughts? Perhaps a better solution?

Thanks,

Christiaan
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Write barrier for stack updates?

[Ömer Sinan Ağacan]

Ah, this makes so much sense, thanks. I was looking at call sites of
recordMutable, recordMutableCap etc. and forgot about recordClosureMutated
which is apparently what dirty_STACK calls.

Thanks,

Ömer

Simon Marlow , 18 Tem 2018 Çar, 10:52 tarihinde şunu yazdı:
>
> Hi Ömer,
>
> The write barrier is the function `dirty_STACK()` here: 
> https://phabricator.haskell.org/diffusion/GHC/browse/master/rts%2Fsm%2FStorage.c$1133-1140
>
> If you grep for `dirty_STACK` you'll see it being called everywhere we mutate 
> a STACK, in particular in the scheduler just before running a thread: 
> https://phabricator.haskell.org/diffusion/GHC/browse/master/rts%2FSchedule.c$412
>
> We don't call the write barrier in the code generator or from primops, 
> because at that point the thread is already running and has already been 
> marked dirty. If we GC and mark the stack clean, then it will be marked dirty 
> again by the scheduler before we start running it.
>
> Cheers
> Simon
>
> On 17 July 2018 at 20:45, Ömer Sinan Ağacan  wrote:
>>
>> Hi Simon,
>>
>> I'm a bit confused about stack updates in generated code and write barriers.
>> Because stacks are mutable (we push new stuff or maybe even update existing
>> frames?) it seems to me that we need one these two, similar to other mutable
>> objects:
>>
>> - Always keep all stacks in mut_lists
>> - Add write barriers before updates
>>
>> However looking at some of the primops like catch# and the code generator 
>> that
>> generates code that pushes update frames I can't see any write barriers and 
>> the
>> GC doesn't always add stacks to mut_lists (unlike e.g. MUT_ARR_PTRS). I also
>> thought maybe we add a stack to a mut_list when we switch to the TSO that 
>> owns
>> it or we park the TSO, but I don't see anything relevant in Schedule.c or
>> ThreadPaused.c. So I'm lost. Could you say a few words about how we deal with
>> mutated stacks in the GC, so that if an old stack points to a young object we
>> don't collect the young object in a minor GC?
>>
>> Thanks,
>>
>> Ömer
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Write barrier for stack updates?

[Simon Marlow]

Hi Ömer,

The write barrier is the function `dirty_STACK()` here:
https://phabricator.haskell.org/diffusion/GHC/browse/master/rts%2Fsm%2FStorage.c$1133-1140

If you grep for `dirty_STACK` you'll see it being called everywhere we
mutate a STACK, in particular in the scheduler just before running a
thread:
https://phabricator.haskell.org/diffusion/GHC/browse/master/rts%2FSchedule.c$412

We don't call the write barrier in the code generator or from primops,
because at that point the thread is already running and has already been
marked dirty. If we GC and mark the stack clean, then it will be marked
dirty again by the scheduler before we start running it.

Cheers
Simon

On 17 July 2018 at 20:45, Ömer Sinan Ağacan  wrote:

> Hi Simon,
>
> I'm a bit confused about stack updates in generated code and write
> barriers.
> Because stacks are mutable (we push new stuff or maybe even update existing
> frames?) it seems to me that we need one these two, similar to other
> mutable
> objects:
>
> - Always keep all stacks in mut_lists
> - Add write barriers before updates
>
> However looking at some of the primops like catch# and the code generator
> that
> generates code that pushes update frames I can't see any write barriers
> and the
> GC doesn't always add stacks to mut_lists (unlike e.g. MUT_ARR_PTRS). I
> also
> thought maybe we add a stack to a mut_list when we switch to the TSO that
> owns
> it or we park the TSO, but I don't see anything relevant in Schedule.c or
> ThreadPaused.c. So I'm lost. Could you say a few words about how we deal
> with
> mutated stacks in the GC, so that if an old stack points to a young object
> we
> don't collect the young object in a minor GC?
>
> Thanks,
>
> Ömer
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs