« Home

Notes [notes]

Naturality cannot be given by a family of isomorphisms [math-000S]

This is came from when I'm formalizing lemma 1.3.11 of Basic Category Theory, I miss a precondition (HH below must be a natural transformation in the lemma) and try to prove an impossible thing.

Let F,G:CDF, G : \mathcal{C} \to \mathcal{D} be functors, and a family

H:(X:C)FXGXH : (X : C) \mapsto F X \cong G X

Does HH must be natural?

Counterexample. [math-000T]

The result is HH can be not natural.

This counterexample is given by Zhixuan Yang:

Let C\mathcal{C} be the two-object one-arrow category, and D\mathcal{D} be SetSet , and

F,G:012id2F, G : 0 \to 1 \mapsto 2 \xrightarrow{id} 2

where 22 is the two elements set. For 00 we choice H(0)=idH(0) = id and H(1)=notH(1) = \text{not} , then HH is not natural.

Definition. exterior algebra [math-000R]

The exterior algebra of vector space VV is defined as a Z\mathbb{Z} -graded algebra:

ΛV:=r0ΛrV\Lambda^\bullet V := \bigoplus_{r \ge 0} \Lambda^r V

Definition. Pfaffian [math-000P]

Let AA be a skew-symmetric endomorphism of a vector space VV (hence AA can also be view as a tensor: AΛ2VA \in \Lambda^2 V ) and N=dimVN = \dim{V} is even, the Pfaffian of AA is the number Pf A\text{Pf}\ A defined as the constant factor in the tensor equality:

(Pf A)e1eN=1(N/2)!AAN/2 times(\text{Pf}\ {A}) e_1 \wedge \dots \wedge e_N = \frac{1}{(N/2)!} \underbrace{A \wedge \dots \wedge A}_{N/2\ times}

where {e1,,eN}\set{e_1,\dots,e_N} is an orthonormal basis of VV .

The sign of Pfaffian depends on the orientation of the orthonormal basis.

Definition. Homotopy extension property (HEP) [math-000O]

A map i:AXi : A \to X of spaces has the homotopy extension property for a space YY if

  1. for each homotopy H:A×IYH : A \times I \to Y
  2. and for each map f:XYf : X \to Y with f(i(a))=H(a,0)f(i(a)) = H(a, 0) for all aAa \in A

there is a homotopy H:X×IYH' : X \times I \to Y such that

H(i(a),t)=H(a,t)H(x,0)=f(x)\begin{align*} &H'(i(a), t) &= &H(a, t) \\ &H'(x, 0) &= &f(x) \end{align*}

for all aAa \in A , xXx \in X and tIt \in I . The idea can be expressed in the following commutative diagram:

figure tex808

The homotopy HH' is called the extension of HH with initial condition ff .

Definition. Natural Transformation [math-000N]

Let C\mathcal{C} and D\mathcal{D} be categories, let F,G:CDF, G : \mathcal{C} \to \mathcal{D} be functors. A natural transformation α:FG\alpha : F \Rightarrow G is a function consists of

  1. For each XCX \in \mathcal{C} , there is a morphism αX:F(X)G(X)\alpha_X : F(X) \to G(X) in D\mathcal{D} , called the XX -component of α\alpha
  2. For every morphism f:XYf : X \to Y in C\mathcal{C} , there is a commute diagram
    figure tex808

常青筆記的困難 [note-0001]

Sterling 的 https://www.forester-notes.org/QHXX/index.xml 精確的描述了常青筆記可能遭遇的困難,關鍵在於,常青筆記對於不停變化的目標,如數學、電腦程式框架等存在,本體論的目標並不統一。用數學為例,我們傳統上接受 ZFC 作為「集合論」的本體,但 topos theory 的發展給出另一套定義 ETCS https://en.wikipedia.org/wiki/Elementary_Theory_of_the_Category_of_Sets!ETCS 說我們覺得集合論是「由 sets 與 functions 構成的 well-pointed topos,有自然數 object 與 Epics split」。

這個定義並沒有循環定義(但使用了短語簡化說法),因為 sets 跟 functions 的公理可以直接給出,ETCS 並沒有比 ZFC 不穩固。

事實上我們甚至知道 ETCS 跟 ZFC 的差異,ETCS + replacement(https://en.wikipedia.org/wiki/Axiom_schema_of_replacement)等價於 ZFC 的推理能力。ZFC 中的某部份等價於 ETCS(參考 Sheaves in Geometry and Logic: A First Introduction to Topos Theory VI. 10)

重點是,既然沒辦法保證討論主題的永久不變,那就應該紀錄當下對主題的洞見,因而在未來仍可從思想中復原出結構。

An Agda Framework for Synthetic Mathematics [math-000K]

Theorem. Borsuk–Ulam [math-000L]

If f:SnRnf : S^n \to \R^n is continuous then there exists a point xSnx \in S^n such that f(x)=f(x)f(x) = f(-x) .

Lemma. [math-000M]

If f:SnRnf : S^n \to \R^n is continuous and antipode-preserving, then there exists a point xSnx \in S^n such that f(x)=0f(x) = 0 .

Proof

Use standard stereographic projection, we can see NN and SS charts gives exactly the same coordinate system at equator (i.e. where its embedding coordinate (x1,,xn+1)(x_1, \dots, x_{n+1}) with xn+1=0x_{n+1} = 0 ). This also tells the equator is a Sn1S^{n-1} in Rn\R^n because x12++xn2=1x_1^2 + \dots + x_n^2 = 1 .

By continuous and antipode-preserving, ff preserves such an equator (we denote EE ) to Sn1S^{n-1} (with scale) and f(E)f(E) must bound a set contains 0Rn0 \in \R^n .

By continuous, both of two open sets of SnS^n , complement of EE , needs to be mapped to cover the subset of Rn\R^n which bounded by f(E)f(E) , so there exists a point xSnx \in S^n such that f(x)=0f(x) = 0 .

Proof

Define g(x)=f(x)f(x)g(x) = f(x) - f(-x) , gg is continuous.

By

g(x)=f(x)f(x)=(f(x)f(x))=g(x)g(x) = f(x) - f(-x) = -(f(x) - f(-x)) = -g(-x)

gg is antipode-preserving.

By the lemma, there is a point xSnx \in S^n such that g(x)=0g(x) = 0 , so f(x)f(x)=0f(x) - f(-x) = 0 then f(x)=f(x)f(x) = f(-x) .

What I Wish I Knew When Learning HoTT [tt-000P]

Lecture. Domain Theory [dt-0000]

Course. CS208 Logic & Algorithms [MSP-cs208]

Tool. agda 的開發工具 [agda-0001]

我使用的編輯器工具是 Agda Mode on VS Code,也可以用 emacs 之類的。常用操作有

  • ctrl+c, ctrl+l 會編譯檢查檔案,假設程式中有 ?,會被替換成所謂的 hole {! !},其實就是待寫的程式

  • ctrl+c, ctrl+, 可以窺看 hole 的目標類型,與當前 context 有哪些 term 可用

  • ctrl+c, ctrl+r 會把 hole 中你打的程式碼往前提取,當然前提是類型是正確的

  • ctrl+c, ctrl+m 會把 hole 中你打的程式碼直接當成結果,一樣類型要是正確的

  • 一般來說一個 agda 定義如下

    hello : A → B
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              hello a = {! !}

    ctrl+c, ctrl+c 會問你要把哪個變數用構造子分開,回答 a,假設有 a1a2 兩個構造子,程式就會變成

    hello : A → B
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              hello a1 = {! !}
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              hello a2 = {! !}
使用 Linux 的使用者可以更改預設的 copy/cut 指令以免衝突。

已完成的軟體 [software-0007]

已完成的軟體這種概念,是指一個軟體的功能已經沒有大幅度更動的必要,可以長期使用在產品上,而軟體本身只會進行必要的安全與移植性更新。我在 https://josem.co/the-beauty-of-finished-software/ 讀到這個想法。對應到筆記軟體上,我不希望軟體一直更新,尤其是當我一打開工具需要寫筆記時,上面的更新按鈕非常的讓人煩躁。同時,這個想法也是一種解放我們原先對軟體想像的開端,比起軟體如何如何,更重要的是真的去做,外部連結裡面也談到冰與火之歌正是用這樣的軟體寫出。

git send-email setup with Protonmail [software-0006]

In the original setup I already explain the configuration, to do the same with Protonmail will need to install Proton Mail Bridge(https://proton.me/mail/bridge), then with configuration as below.

[sendemail]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpEncryption = STARTTLS
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpServer = 127.0.0.1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpUser = @protonmail.com
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpServerPort = 1025
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpPass = 

Definition. point-surjective [math-000A]

A morphism AϕBA \xrightarrow{\phi} B is point-surjective iff for every point 1qB1 \xrightarrow{q} B , there exists a point 1pA1 \xrightarrow{p} A that lifts qq (satisfy ϕp=q\phi \circ p = q ).

git send-email 的設定 [software-0004]

I use gmail, and hence, I need to get a Google app password. After having the password, one has to setup ~/.gitconfig with content:

[sendemail]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpEncryption = tls
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpServer = smtp.gmail.com
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpUser = @gmail.com
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpServerPort = 587
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                smtpPass = 

Then you are able to use \code{git send-email} command:

git switch -c branch-patch
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              git format-patch main
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              git send-email 0001-***********.patch

prompt will ask some questions, an important one is which mailing list is your target? After command success, your patch are sent.

For certain git repository you're working on, can config local repository via \code{git config --edit}, and add below to omit email list in command line.

[sendemail]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                to = 

Mastodon 私訊相比於一般通訊軟體 e.g. LINE, Telegram [software-0003]

好處

  1. 可以有效分類特定話題,例如一個串是講約去哪裡吃飯、另一個串講專業內容
  2. 可以用僅限提及的人,限制可見性,所以可以形成一定程度的群組概念

壞處

  1. 兩方站點的站長都能看到內容
  2. 客戶端不支援把一群提及名單固定成群組,這或許是一個可行的客戶端新功能

壞處的可能解法:公佈自己的 public key 讓對方加密訊息再傳,配上專用客戶軟體或許可以做的更方便

let Racket GC manage your FFI object [software-0005]

All you need are deallocator and allocator from ffi/unsafe/alloc.

(require ffi/unsafe
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       ffi/unsafe/define
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                       ffi/unsafe/alloc)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (define-ffi-definer define-xxx
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                (ffi-lib "" '(#f)))

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (define-xxx free-yyy (_fun _YyyRef -> _void)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                #:c-id yyy_delete
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                #:wrap (deallocator))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              (define-xxx make-yyy (_fun -> _YyyRef)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                #:c-id yyy_new
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                #:wrap (allocator free-yyy))

Tool. ngrok [software-0002]

Sometimes we didn't have public ip, but temporary wants to test website, ngrok can help in this situation.

# expose localhost:8080 by HTTP
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              $ ngrok http 8080
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              # expose localhost:8080 by TCP
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              $ ngrok tcp 8080

XDP [software-0001]

XDP is eXpress Data Path, it's a technology about putting a BPF code virtual machine on the NIC(network interface controller) driver before kernel network stack so that we can filter the packet before kernel, it would make processing speed greater.

We can do following things on the packet:

  1. XDP_PASS: allow the packet to pass through
  2. XDP_DROP: drop the packet
  3. XDP_TX: bounce the packet back on the same interface
  4. XDP_REDIRECT: redirects the packet to another interface

Here is an example of counting how many IPv4/6 packets be dropped.

package main

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              import (
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  "fmt"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  "os"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  "os/signal"

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  bpf "github.com/iovisor/gobpf/bcc"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              )

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              // bcc is from iovisor/bcc this project
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              /*
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #cgo CFLAGS: -I/usr/include/bcc/compat
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #cgo LDFLAGS: -lbcc
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              void perf_reader_free(void *ptr);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              */
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              import "C"

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              const source string = `
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #define KBUILD_MODNAME "foo"
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              #include 
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              BPF_TABLE("array", int, long, dropcnt, 256);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              static inline int parse_ipv4(void *data, u64 nh_off, void *data_end) {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  struct iphdr *iph = data + nh_off;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if ((void*)&iph[1] > data_end)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      return 0;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  return iph->protocol;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              static inline int parse_ipv6(void *data, u64 nh_off, void *data_end) {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  struct ipv6hdr *ip6h = data + nh_off;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if ((void*)&ip6h[1] > data_end)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      return 0;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  return ip6h->nexthdr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              int xdp_prog1(struct xdp_md *ctx) {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  void* data_end = (void*)(long)ctx->data_end;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  void* data = (void*)(long)ctx->data;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  struct ethhdr *eth = data;

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  uint64_t nh_off = sizeof(*eth);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if (data + nh_off  > data_end)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      return XDP_DROP;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  uint16_t h_proto = eth->h_proto;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if (h_proto == htons(ETH_P_8021Q) || h_proto == htons(ETH_P_8021AD)) {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      struct vlan_hdr *vhdr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      vhdr = data + nh_off;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      nh_off += sizeof(struct vlan_hdr);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      if (data + nh_off > data_end)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          return XDP_DROP;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          h_proto = vhdr->h_vlan_encapsulated_proto;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if (h_proto == htons(ETH_P_8021Q) || h_proto == htons(ETH_P_8021AD)) {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      struct vlan_hdr *vhdr;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      vhdr = data + nh_off;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      nh_off += sizeof(struct vlan_hdr);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      if (data + nh_off > data_end)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          return XDP_DROP;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          h_proto = vhdr->h_vlan_encapsulated_proto;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  int index;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if (h_proto == htons(ETH_P_IP))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      index = parse_ipv4(data, nh_off, data_end);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  else if (h_proto == htons(ETH_P_IPV6))
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      index = parse_ipv6(data, nh_off, data_end);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  else
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      index = 0;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  long *value;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  value = dropcnt.lookup(&index);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if (value) lock_xadd(value, 1);
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  return XDP_DROP;
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              `

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              func usage() {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  fmt.Printf("Usage: %v \n", os.Args[0])
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  fmt.Printf("e.g.: %v eth0\n", os.Args[0])
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  os.Exit(1)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              }

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              func main() {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if len(os.Args) != 2 {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      usage()
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  module := bpf.NewModule(source, []string{
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      "-w",
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  })
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  defer module.Close()

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  fn, err := module.Load("xdp_prog1", C.BPF_PROG_TYPE_XDP, 1, 65536)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if err != nil {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      fmt.Fprintf(os.Stderr, "Failed to load xdp prog: %v\n", err)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      os.Exit(1)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  device := os.Args[1]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  if err := module.AttachXDP(device, fn); err != nil {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      fmt.Fprintf(os.Stderr, "Failed to attach xdp prog: %v\n", err)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      os.Exit(1)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  defer func() {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      if err := module.RemoveXDP(device); err != nil {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          fmt.Fprintf(os.Stderr, "Failed to remove XDP from %s: %v\n", device, err)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }()

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  fmt.Println("Dropping packets, hit CTRL+C to stop")
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  sig := make(chan os.Signal, 1)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  signal.Notify(sig, os.Interrupt, os.Kill)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  dropcnt := bpf.NewTable(module.TableId("dropcnt"), module)

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  <-sig

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  fmt.Println("\n{IP protocol-number}: {total dropped pkts}")
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  for it := dropcnt.Iter(); it.Next(); {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      key := bpf.GetHostByteOrder().Uint32(it.Key())
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      value := bpf.GetHostByteOrder().Uint64(it.Leaf())

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      if value > 0 {
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          fmt.Printf("%v: %v pkts\n", key, value)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              }

Algorithm. Mark sweep GC [cs-0008]

Mark-Sweep is a classic GC algorithm, it's combined with two parts, mark and sweep.

mark(root):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          if not marked?(root):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            mark(root)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          for obj in knowns(root):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            mark(obj)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        sweep(heap):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          for obj in heap:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            if marked?(obj):
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              unmark(obj)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            else:
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              release(obj)

If we run collection (mark-sweep), then since each object is reachable from root, so no one would be released.

figure tex808

After do some executions, obj1 don't need obj3 anymore, so it became:

figure tex809

Now when we run collection, obj3 is unreachable from root, so it won't be marked! When running to sweep, it will be dropped.