wilbowma

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)

RealNeGate

// Compile with clang or MSVC (WINDOWS ONLY RN)
//
// Implementing a POC green threads system using safepoints to show how cheap and simple it can
// be done, all you need to do is call SAFEPOINT_POLL in your own language at the top of every
// loop and function body (you can loosen up on this depending on the latency of pausing you're
// willing to pay). Safepoint polling is made cheap because it's a load without a use site
// which means it doesn't introduce a stall and pays a sub-cycle cost because of it (wastes resources
// sure but doesn't block up the rest of execution).
//
//  # safepoint poll

isti115

{-# OPTIONS --rewriting #-}
module sknorm where

open import Agda.Primitive
open import Level
open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Equality.Rewrite
open import Data.Product
open import Data.Empty

pervognsen

// Estimating CPU frequency...
// CPU frequency: 4.52 GHz
// sum1: value = 15182118497126522709, 0.31 secs, 5.14 cycles/elem
// sum2: value = 15182118497126522709, 0.17 secs, 2.93 cycles/elem

#define RW(x) asm("" : "+r"(x))

typedef struct Node {
	u64 value;
	struct Node *next;

vivshaw

If you want to see how it works, see the README on the repo.

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

MattPD

Program Analysis Resources

(draft; work in progress)

See also:

• Compilers
  • correctness
• Program analysis:
• Dynamic analysis - instrumentation, translation, sanitizers

fairlight1337

// This code installs a custom signal handler for the SIGSEGV signal
// (segmentation fault) and then purposefully creates a segmentation
// fault. The custom handler `handler` is then entered, which now
// increases the instruction pointer by 1, skipping the current byte
// of the faulty instruction. This is done for as long as the faulty
// instruction is still active; in the below case, that's 2 bytes.

// Note: This is for 64 bit systems. If you prefer 32 bit, change
// `REG_RIP` to `REG_EIP`. I didn't bother putting an appropriate
// `#ifdef` here.

chrisdone

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

larrytheliquid

open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
  renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
    renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )