Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add feedback-guided scheduling algorithms #791

Merged
merged 29 commits into from
Oct 18, 2024
Merged

Conversation

aoli-al
Copy link
Contributor

@aoli-al aoli-al commented Oct 10, 2024

This PR introduces the following scheduling algorithm:

  • POS
  • Feedback-POS
  • Feedback-PCT
  • Feedback-Random

aoli-al and others added 12 commits April 8, 2024 14:56
* Add feedback guided scheduling algorithms.

* Fix tests.

* Add location information to events.

* fix change.
* Disable trace logging to save disk space.

* Update feedback algorithm.

* fix feedback strategy.

* refactor.

* Remove experiment features.

---------

Co-authored-by: Ao Li <[email protected]>
* Added support for generating a warning when spec handles an event but does not add it in its observes list (#716)

* Create custom converter for JSON serialization in .NET8 (#717)

* Create custom converter for JSON serialization in .NET8

* Add check for different dictionary type for null replacement

---------

Co-authored-by: Eric Hua <[email protected]>

---------

Co-authored-by: Ankush Desai <[email protected]>
Co-authored-by: Eric Hua <[email protected]>
Co-authored-by: Eric Hua <[email protected]>
* Added support for generating a warning when spec handles an event but does not add it in its observes list (#716)

* Create custom converter for JSON serialization in .NET8 (#717)

* Create custom converter for JSON serialization in .NET8

* Add check for different dictionary type for null replacement

---------

Co-authored-by: Eric Hua <[email protected]>

* udpate.

* update.

* update.

---------

Co-authored-by: Eric Hua <[email protected]>
Co-authored-by: Eric Hua <[email protected]>
Co-authored-by: Ao Li <[email protected]>
Co-authored-by: Christine Zhou <[email protected]>
Co-authored-by: Christine Zhou <[email protected]>
Src/PChecker/CheckerCore/CheckerConfiguration.cs Outdated Show resolved Hide resolved
Src/PChecker/CheckerCore/Actors/Logging/JsonWriter.cs Outdated Show resolved Hide resolved
Src/PChecker/CheckerCore/CheckerConfiguration.cs Outdated Show resolved Hide resolved

internal class RandomScheduleMutator : IMutator<RandomScheduleGenerator>
{
private readonly int _meanMutationCount = 10;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why these values 10 and not something else?

@ankushdesai ankushdesai self-requested a review October 16, 2024 23:45
@ankushdesai
Copy link
Member

Based on the discussion today, can @aoli-al you please do the following refactoring:

  1. Merge all the mutators into a single mutator that mutates schedules irrespective of the scheduler.
  2. Remove the changes in the Probabilistic folder to remove the changes associated with Scheduler and Provider. We are not sure if we need to introduce the PrioritizedProvider interface.

where T: IConvertible
{
internal readonly System.Random Random;
public int Pos;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There seems to be bug here, pos is never initialized to 0?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not necessary. Pos is default to 0 during initialization.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How and where?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

}

/// <inheritdoc/>
public uint Seed { get; set; }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When is this Seed being set?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seed is not used in ControlledRandom. This field is added to implement the IRandomValueGenerator interface


public ControlledRandom Mutate()
{
return new ControlledRandom(Utils.MutateRandomChoices(IntChoices, 5, 5, IntChoices.Random),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we only mutate only 5 times?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a hyper-parameter. 5 is the mean mutation count and mean mutation size here. Not a fixed number.

@aoli-al aoli-al requested a review from ankushdesai October 18, 2024 07:30
@ankushdesai ankushdesai merged commit b45194b into master Oct 18, 2024
8 checks passed
@ankushdesai ankushdesai deleted the experimental/feedback branch October 18, 2024 20:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants